---

Step * of Lemma div_induction-ext

∀b:{b:ℤ| 1 < b} . ∀[P:ℤ ⟶ ℙ]. (P[0] ⇒ (∀i:ℤ-o. (P[i ÷ b] ⇒ P[i])) ⇒ (∀i:ℤ. P[i]))
BY
{ Extract of Obid: div_induction
  not unfolding  divide absval natrec
  finishing with Auto
  normalizes to:
  
  λb,x,f,i. letrec F(i)=if i=0 then x else eval i' = i ÷ b in f i (F i') in F(i) }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  div\_induction
not  unfolding    divide  absval  natrec
finishing  with  Auto
normalizes  to:

\mlambda{}b,x,f,i.  letrec  F(i)=if  i=0  then  x  else  eval  i'  =  i  \mdiv{}  b  in  f  i  (F  i')  in  F(i)

---

Home Index