---

Step * of Lemma div_nat_induction-ext

∀b:{b:ℤ| 1 < b} . ∀[P:ℕ ⟶ ℙ]. (P[0] ⇒ (∀i:ℕ+. (P[i ÷ b] ⇒ P[i])) ⇒ (∀i:ℕ. P[i]))
BY
{ Extract of Obid: div_nat_induction
  not unfolding  divide 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) }

---

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:
Extract  of  Obid:  div\_nat\_induction
not  unfolding    divide  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)

---

Home Index