---

Step * of Lemma int-sqrt-ext

∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
BY
{ xxxExtract of Obid: int-sq-root
     normalizes to:
     
     λx.letrec F(x)=if x=0
                    then 0
                    else eval z = x ÷ 4 in
                         eval 2r = 2 * (F z) in
                         eval 2r' = 2r + 1 in
                           if (x) < (2r' * 2r')  then 2r  else 2r' in
         F(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:  int-sq-root
      normalizes  to:
     
      \mlambda{}x.letrec  F(x)=if  x=0
                                    then  0
                                    else  eval  z  =  x  \mdiv{}  4  in
                                              eval  2r  =  2  *  (F  z)  in
                                              eval  2r'  =  2r  +  1  in
                                                  if  (x)  <  (2r'  *  2r')    then  2r    else  2r'  in
              F(x)
      finishing  with  Autoxxx

---

Home Index