---

Step * of Lemma fun_exp_add1

∀[f,x:Top]. ∀[n:ℕ].  (f (f^n x) ~ f^n + 1 x)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `fun_exp` 0
   THEN (RW (AddrC [2;1] (LemmaC `primrec-unroll`)) 0 THENA Auto)
   THEN (SplitOnConclITE THENA Auto)
   THEN Fold `fun_exp` 0
   THEN Reduce 0
   THEN Try (Complete (Auto'))
   THEN RepeatFor 3 (EqCD)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f,x:Top].  \mforall{}[n:\mBbbN{}].    (f  (f\^{}n  x)  \msim{}  f\^{}n  +  1  x)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `fun\_exp`  0
  THEN  (RW  (AddrC  [2;1]  (LemmaC  `primrec-unroll`))  0  THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Fold  `fun\_exp`  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto'))
  THEN  RepeatFor  3  (EqCD)
  THEN  Auto)

---

Home Index