Library FunG_prog: Alternative definition of Hofstadter's G function
Require Import FunG.
Require Import Arith Omega Wf_nat List Program Program.Wf.
Set Implicit Arguments.
Same as FunG.g_spec, but via the Program framework
Program Fixpoint g_spec n { measure n } : { r : nat | G n r } :=
match n with
| O ⇒ O
| S n ⇒ S n - g_spec (g_spec n)
end.
Definition g n := let (a,_) := g_spec n in a.
This is just an alternative presentation...