---

Step * 2 1 of Lemma sqrt-int-aa-fast


1. i : @i
2. r : @i
3. ((r * r)  (i  4))  ((i  4) < ((r + 1) * (r + 1)))@i
 r:. (((r * r)  i)  (i < ((r + 1) * (r + 1))))
BY
{ ((Assert Dec(i < (((2 * r) + 1) * ((2 * r) + 1))) BY Auto) THEN D (-1)) }

1
1. i : @i
2. r : @i
3. ((r * r)  (i  4))  ((i  4) < ((r + 1) * (r + 1)))@i
4. i < (((2 * r) + 1) * ((2 * r) + 1))
 r:. (((r * r)  i)  (i < ((r + 1) * (r + 1))))

2
1. i : @i
2. r : @i
3. ((r * r)  (i  4))  ((i  4) < ((r + 1) * (r + 1)))@i
4. (i < (((2 * r) + 1) * ((2 * r) + 1)))
 r:. (((r * r)  i)  (i < ((r + 1) * (r + 1))))



1.  i  :  \mBbbN{}@i
2.  r  :  \mBbbN{}@i
3.  ((r  *  r)  \mleq{}  (i  \mdiv{}  4))  \mwedge{}  ((i  \mdiv{}  4)  <  ((r  +  1)  *  (r  +  1)))@i
\mvdash{}  \mexists{}r:\mBbbN{}.  (((r  *  r)  \mleq{}  i)  \mwedge{}  (i  <  ((r  +  1)  *  (r  +  1))))


By

((Assert  Dec(i  <  (((2  *  r)  +  1)  *  ((2  *  r)  +  1)))  BY  Auto)  THEN  D  (-1))



Home Index