---

Step * of Lemma accum-induction-ext

∀[P:ℕ ⟶ ℙ]. (P[0] ⇒ (∀n:ℕ. (P[n] ⇒ P[n + 1])) ⇒ (∀n:ℕ. P[n]))
BY
{ xxxNormalizeExtractTo (ioid Obid: accum-induction)⌜λb,f,n. (primrec(n;λ_,y. y;λ_,p,m,y. (p (m + 1) (f m y))) 0 b)⌝
 100 ``primrec``⋅xxx }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (P[0]  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (P[n]  {}\mRightarrow{}  P[n  +  1]))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  P[n]))


By

---

Latex:
xxxNormalizeExtractTo  (ioid  Obid:  accum-induction)\mkleeneopen{}\mlambda{}b,f,n.  (primrec(n;\mlambda{}$_{}$,y.  \000Cy;\mlambda{}$_{}$,p,m,y.  (p  (m  +  1) 
                                                                                                                                                                        (f  m  y))) 
                                                                                                                        0 
                                                                                                                        b)\mkleeneclose{}
  100  ``primrec``\mcdot{}xxx

---

Home Index