---

Step * of Lemma isqrrrt-program

∀n:ℕ. (∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))])
BY
{ Extract of Obid: isqrrrt
  normalizes to:
  
  λi.letrec F(i)=if i=0
                 then 0
                 else let x,r = divrem(i; 4) 
                      in eval z = x in
                         eval r2 = 2 * (F z) in
                         eval r3 = r2 + 1 in
                           if (i) < (r3 * r3)  then r2  else r3 in
      F(i)
  finishing with Auto }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  isqrrrt
normalizes  to:

\mlambda{}i.letrec  F(i)=if  i=0
                              then  0
                              else  let  x,r  =  divrem(i;  4) 
                                        in  eval  z  =  x  in
                                              eval  r2  =  2  *  (F  z)  in
                                              eval  r3  =  r2  +  1  in
                                                  if  (i)  <  (r3  *  r3)    then  r2    else  r3  in
        F(i)
finishing  with  Auto

---

Home Index