---

Step * of Lemma natInd4Boot44

P:  . (((P 0)  (i:. ((P (i  4))  (P i))))  (n:. (P n)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN D (-1)
   THEN RenameVar `base' (-2)
   THEN RenameVar `ind' (-1)
   THEN UseWitness letrec rec(n)=if n=0  then base  else (ind n (rec (n  4))) in
                     rec
   THEN Auto
   THEN BLemma `div_mono1`
   THEN Auto) }


\mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  (((P  0)  \mwedge{}  (\mforall{}i:\mBbbN{}.  ((P  (i  \mdiv{}  4))  {}\mRightarrow{}  (P  i))))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (P  n)))


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  (-1)
  THEN  RenameVar  `base'  (-2)
  THEN  RenameVar  `ind'  (-1)
  THEN  UseWitness  \mkleeneopen{}letrec  rec(n)=if  n=0    then  base    else  (ind  n  (rec  (n  \mdiv{}  4)))  in
                                      rec\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  BLemma  `div\_mono1`
  THEN  Auto)



Home Index