---

Step * of Lemma comp-nat-ind-ext

∀[P:ℕ ⟶ ℙ]. ((∀i:ℕ. ((∀j:ℕi. P[j]) ⇒ P[i])) ⇒ (∀i:ℕ. P[i]))
BY
{ Extract of Obid: complete_nat_ind
  not unfolding  primrec
  finishing with Auto
  normalizes to:
  
  λF,i. (primrec(i + 1;λi.Ax;λi,x,i. (F i (λj.(x j)))) i) }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}i.  P[j])  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}.  P[i]))


By

---

Latex:
Extract  of  Obid:  complete\_nat\_ind
not  unfolding    primrec
finishing  with  Auto
normalizes  to:

\mlambda{}F,i.  (primrec(i  +  1;\mlambda{}i.Ax;\mlambda{}i,x,i.  (F  i  (\mlambda{}j.(x  j))))  i)

---

Home Index