---

Step * of Lemma sqrt-int-aa-real-fast-complete-ext

n:. r:. (((r * r)  n)  (n < ((r + 1) * (r + 1))))
BY
{ NewUseNormalizedExtract ``primrec`` false (ioid Obid: sqrt-int-aa-real-fast-complete) }

1
1. n.letrec f(n)=if n=0
                     then <0, .Ax, Ax>
                     else let r,%1 = f (n  4) 
                          in let %2,%3 = %1 
                             in if (n) < (((2 * r) + 1) * ((2 * r) + 1))
                                   then <2 * r, x.any Ax, Ax>
                                   else <(2 * r) + 1, x.any Ax, Ax> in
       f(n)  n:. r:. (((r * r)  n)  (n < ((r + 1) * (r + 1))))
 n.letrec f(n)=if n=0
                    then <0, .Ax, Ax>
                    else let r,%1 = f (n  4) 
                         in let %2,%3 = %1 
                            in if (n) < (((2 * r) + 1) * ((2 * r) + 1))
                                  then <2 * r, x.any Ax, Ax>
                                  else <(2 * r) + 1, x.any Ax, Ax> in
      f(n)  n:. r:. (((r * r)  n)  (n < ((r + 1) * (r + 1))))


\mforall{}n:\mBbbN{}.  \mexists{}r:\mBbbN{}.  (((r  *  r)  \mleq{}  n)  \mwedge{}  (n  <  ((r  +  1)  *  (r  +  1))))


By

NewUseNormalizedExtract  ``primrec``  false  (ioid  Obid:  sqrt-int-aa-real-fast-complete)\mcdot{}



Home Index