---

Step * of Lemma int-sqrt-ext

∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
BY
{ Extract of Obid: int-sq-root
  not unfolding  divide
  finishing with Auto
  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) }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  int-sq-root
not  unfolding    divide
finishing  with  Auto
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)

---

Home Index