---

Step * of Lemma div_nat_induction-ext

∀b:{b:ℤ| 1 < b} . ∀[P:ℕ ⟶ ℙ]. (P[0] ⇒ (∀i:ℕ+. (P[i ÷ b] ⇒ P[i])) ⇒ (∀i:ℕ. P[i]))
BY
{ xxxExtract of Obid: div_nat_induction
     not unfolding  natrec
     finishing with Auto
     normalizes to:
     
     λb,p0,pfun,i. (letrec F(i)=if i=0 then p0 else eval z = i ÷ b in pfun i (F z) in F i)xxx }

---

Latex:

---

Latex:
\mforall{}b:\{b:\mBbbZ{}|  1  <  b\}  .  \mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (P[0]  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}\msupplus{}.  (P[i  \mdiv{}  b]  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}.  P[i]))


By

---

Latex:
xxxExtract  of  Obid:  div\_nat\_induction
      not  unfolding    natrec
      finishing  with  Auto
      normalizes  to:
     
      \mlambda{}b,p0,pfun,i.  (letrec  F(i)=if  i=0  then  p0  else  eval  z  =  i  \mdiv{}  b  in  pfun  i  (F  z)  in  F  i)xxx

---

Home Index