---

Step * of Lemma integer-sqrt-newton-ext

∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
BY
{ xxxExtract of Obid: integer-sqrt-newton
     not unfolding 
     finishing with Auto
     normalizes to:
     
     λx.if x=0
        then 0
        else letrec isqrt_newton(n)=eval s = n + (x ÷ n) in
                                    eval z = s ÷ 2 in
                                      if z=n then z else if (n) < (z)  then n  else (isqrt_newton z) in
              isqrt_newton(x)xxx }

---

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-newton
      not  unfolding 
      finishing  with  Auto
      normalizes  to:
     
      \mlambda{}x.if  x=0
            then  0
            else  letrec  isqrt$_{newton}$(n)=eval  s  =  n  +  (x  \mdiv{}  n)  in
                                                                  eval  z  =  s  \mdiv{}  2  in
                                                                      if  z=n  then  z  else  if  (n)  <  (z)    then  n    else  (isqrt$_\mbackslash{}ff\000C7bnewton}$  z)  in
                        isqrt$_{newton}$(x)xxx

---

Home Index