---

Step * of Lemma integer-sqrt-newton-ext

∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
BY
{ Extract of Obid: integer-sqrt-newton
  not unfolding 
  finishing with (Unfold `divide` 0 THEN (Auto THEN Unfold `pi1` 0) THEN 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) }

---

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-newton
not  unfolding 
finishing  with  (Unfold  `divide`  0  THEN  (Auto  THEN  Unfold  `pi1`  0)  THEN  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$_{n\000Cewton}$  z)  in
                  isqrt$_{newton}$(x)

---

Home Index