---

Step * of Lemma fun_exp_unroll_1

∀[n:ℕ+]. ∀[f:Top].  (f^n ~ λx.(f (f^n - 1 x)))
BY
{ (InstLemma `fun_exp_unroll` []
   THEN RepeatFor 2 (ParallelLast')
   THEN UseWitness ⌜Ax⌝⋅
   THEN MemCD
   THEN AddHiddenLabel`main`) }

1
1. n : ℕ+
2. f : Top
3. f^n ~ if (n =z 0) then λx.x else f o f^n - 1 fi 
⊢ f^n ~ λx.(f (f^n - 1 x))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[f:Top].    (f\^{}n  \msim{}  \mlambda{}x.(f  (f\^{}n  -  1  x)))


By

---

Latex:
(InstLemma  `fun\_exp\_unroll`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  MemCD
  THEN  AddHiddenLabel`main`)

---

Home Index