---

Step * of Lemma integer-sqrt-ext

∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
BY
{ xxxExtract of Obid: integer-sqrt
     normalizes to:
     
     λx.letrec rec(i)=if i=0
                      then 0
                      else eval j = i ÷ 4 in
                           eval r2 = 2 * (rec j) in
                           eval r2' = r2 + 1 in
                             if (r2' * r2') < (i + 1)  then r2'  else r2 in
         rec(x)
     finishing with Autoxxx }

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}.  (\mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)  *  (r  +  1))])


By

---

Latex:
xxxExtract  of  Obid:  integer-sqrt
      normalizes  to:
     
      \mlambda{}x.letrec  rec(i)=if  i=0
                                        then  0
                                        else  eval  j  =  i  \mdiv{}  4  in
                                                  eval  r2  =  2  *  (rec  j)  in
                                                  eval  r2'  =  r2  +  1  in
                                                      if  (r2'  *  r2')  <  (i  +  1)    then  r2'    else  r2  in
              rec(x)
      finishing  with  Autoxxx

---

Home Index