---

Step * 1 1 of Lemma sqrt-int-aa-real-fast-complete-ext


1. n.letrec f(n)=if n=0
                     then <0, .Ax, Ax>
                     else let r,%1 = f (n  4) 
                          in let %2,%3 = %1 
                             in if (n) < (((2 * r) + 1) * ((2 * r) + 1))
                                   then <2 * r, x.any Ax, Ax>
                                   else <(2 * r) + 1, x.any Ax, Ax> in
       f(n)  n:. r:. (((r * r)  n)  (n < ((r + 1) * (r + 1))))
 n.(fix((f,n. if n=0
                    then <0, .Ax, Ax>
                    else let r,%1 = f (n  4) 
                         in let %2,%3 = %1 
                            in if (n) < (((2 * r) + 1) * ((2 * r) + 1))
                                  then <2 * r, x.any Ax, Ax>
                                  else <(2 * r) + 1, x.any Ax, Ax>)) 
      n)  n:. r:. (((r * r)  n)  (n < ((r + 1) * (r + 1))))
BY
{ (Fold `genrec-ap` 0 THEN Auto) }



1.  \mlambda{}n.letrec  f(n)=if  n=0
                                          then  ɘ,  \mlambda{}.Ax,  Ax>
                                          else  let  r,\%1  =  f  (n  \mdiv{}  4) 
                                                    in  let  \%2,\%3  =  \%1 
                                                          in  if  (n)  <  (((2  *  r)  +  1)  *  ((2  *  r)  +  1))
                                                                      then  ɚ  *  r,  \mlambda{}x.any  Ax,  Ax>
                                                                      else  <(2  *  r)  +  1,  \mlambda{}x.any  Ax,  Ax>  in
              f(n)  \mmember{}  \mforall{}n:\mBbbN{}.  \mexists{}r:\mBbbN{}.  (((r  *  r)  \mleq{}  n)  \mwedge{}  (n  <  ((r  +  1)  *  (r  +  1))))
\mvdash{}  \mlambda{}n.(fix((\mlambda{}f,n.  if  n=0
                                        then  ɘ,  \mlambda{}.Ax,  Ax>
                                        else  let  r,\%1  =  f  (n  \mdiv{}  4) 
                                                  in  let  \%2,\%3  =  \%1 
                                                        in  if  (n)  <  (((2  *  r)  +  1)  *  ((2  *  r)  +  1))
                                                                    then  ɚ  *  r,  \mlambda{}x.any  Ax,  Ax>
                                                                    else  <(2  *  r)  +  1,  \mlambda{}x.any  Ax,  Ax>)) 
            n)  \mmember{}  \mforall{}n:\mBbbN{}.  \mexists{}r:\mBbbN{}.  (((r  *  r)  \mleq{}  n)  \mwedge{}  (n  <  ((r  +  1)  *  (r  +  1))))


By

(Fold  `genrec-ap`  0\mcdot{}  THEN  Auto)



Home Index