---

Step * 1 1 2 1 of Lemma natInd4BootFast


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
7. (n1 = 0)
 (n1  4) < n1
BY
{ ((InstLemma `div_rem_sum` [n1;4] THENA Auto) THEN (InstLemma `rem_bounds_1` [n1;4] THENA 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
7. (n1 = 0)
8. n1 = (((n1  4) * 4) + (n1 rem 4))
9. (0  (n1 rem 4))  ((n1 rem 4) < 4)
 (n1  4) < 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
5.  n1  :  \mBbbN{}@i
6.  \mforall{}m:\mBbbN{}n1.  (P  m)@i
7.  \mneg{}(n1  =  0)
\mvdash{}  (n1  \mdiv{}  4)  <  n1


By

((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}n1\mkleeneclose{};\mkleeneopen{}4\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}n1\mkleeneclose{};\mkleeneopen{}4\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )



Home Index