Step
*
of Lemma
genrec-unroll
∀[g,n:Top].  (letrec f(n)=g[n;f] in f  n ~ g[n;letrec f(n)=g[n;f] in f ])
BY
{ (Auto THEN RW (AddrC [1] (RecUnfoldC `genrec`)) 0  THEN Reduce 0 THEN Auto) }
Latex:
Latex:
\mforall{}[g,n:Top].    (letrec  f(n)=g[n;f]  in  f    n  \msim{}  g[n;letrec  f(n)=g[n;f]  in  f  ])
By
Latex:
(Auto  THEN  RW  (AddrC  [1]  (RecUnfoldC  `genrec`))  0    THEN  Reduce  0  THEN  Auto)
Home
Index