---

Step * of Lemma integer-sqrt-ext

∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
BY
{ Extract of Obid: integer-sqrt
  normalizes to:
  
  λx.letrec rec(i)=if i=0
                   then 0
                   else let x,r = divrem(i; 4) 
                        in eval j = x 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 Auto }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  integer-sqrt
normalizes  to:

\mlambda{}x.letrec  rec(i)=if  i=0
                                  then  0
                                  else  let  x,r  =  divrem(i;  4) 
                                            in  eval  j  =  x  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  Auto

---

Home Index