From Equations Require Import Equations.
Require Import Examples.Fin.

Inductive ho : Set :=
| base : nat → ho
| lim : ∀ n : nat, (fin n → ho) → ho.
Derive NoConfusion for ho.

Equations lift_fin {n : nat} (f : fin n) : fin (S n) :=
lift_fin fz := fz;
lift_fin (fs f) := fs (lift_fin f).

Equations maxf (n : nat) (f : fin n → nat) : nat :=
maxf 0 f := 0;
maxf (S n) f := max (f (gof n)) (maxf n (fun y : fin n ⇒ f (lift_fin y))).

Equations horec_struct (x : ho) : nat :=
horec_struct (base n) := n;
horec_struct (lim k f) := maxf k (fun x ⇒ horec_struct (f x)).

Derive Subterm for ho.

Equations horec (x : ho) : nat by wf x ho_subterm :=
horec (base n) := n;
horec (lim k f) := maxf k (fun x ⇒ horec (f x)).

Definition horec_test : horec (lim 7 (fun fs ⇒ base (fog fs))) = 6 := eq_refl.