Step
*
of Lemma
div_induction-ext
∀b:{b:ℤ| 1 < b} . ∀[P:ℤ ⟶ ℙ]. (P[0] 
⇒ (∀i:ℤ-o. (P[i ÷ b] 
⇒ P[i])) 
⇒ (∀i:ℤ. P[i]))
BY
{ xxxExtract of Obid: div_induction
     not unfolding  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)xxx }
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:
xxxExtract  of  Obid:  div\_induction
      not  unfolding    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)xxx
Home
Index