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