---

Step * 1 of Lemma natInd4Boot


1. P :   @i'
2. P 0@i
3. i:. ((P (i  4))  (P i))@i
4. n : @i
 P n
BY
{ (BLemma `completeInductionBootStrap` THEN Auto) }

1
1. P :   @i'
2. P 0@i
3. i:. ((P (i  4))  (P i))@i
4. n : @i
5. n1 : @i
6. m:n1. (P m)@i
 P n1



1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
2.  P  0@i
3.  \mforall{}i:\mBbbN{}.  ((P  (i  \mdiv{}  4))  {}\mRightarrow{}  (P  i))@i
4.  n  :  \mBbbN{}@i
\mvdash{}  P  n


By

(BLemma  `completeInductionBootStrap`  THEN  Auto)



Home Index