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 else eval i' i ÷ in (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