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