Nuprl Definition : isqrt_newton

isqrt_newton(n;x)
==r eval s = x + (n ÷ x) in
    eval z = s ÷ 2 in
      if z=x then z else if (x) < (z)  then x  else isqrt_newton(n;z)
isqrt_newton(n;x) ==
  fix((λisqrt_newton,x. eval s = x + (n ÷ x) in
                        eval z = s ÷ 2 in
                          if z=x then z else if (x) < (z)  then x  else (isqrt_newton z))) 
  x


Definitions occuring in Statement :  callbyvalue: callbyvalue,  less: if (a) < (b)  then c  else d,  int_eq: if a=b then c else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  divide: n ÷ m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  apply: f a,  less: if (a) < (b)  then c  else d,  int_eq: if a=b then c else d,  natural_number: $n,  divide: n ÷ m,  callbyvalue: callbyvalue,  add: n + m,  lambda: λx.A[x],  fix: fix(F)
FDL editor aliases :  isqrt_newton
Latex:
isqrt\_newton(n;x)
==r  eval  s  =  x  +  (n  \mdiv{}  x)  in
        eval  z  =  s  \mdiv{}  2  in
            if  z=x  then  z  else  if  (x)  <  (z)    then  x    else  isqrt\_newton(n;z)
Latex:
isqrt\_newton(n;x)  ==
    fix((\mlambda{}isqrt$_{newton}$,x.  eval  s  =  x  +  (n  \mdiv{}  x)  in
                                              eval  z  =  s  \mdiv{}  2  in
                                                  if  z=x  then  z  else  if  (x)  <  (z)    then  x    else  (isqrt$_{newton\mbackslash{}f\000Cf7d$  z))) 
    x


Date html generated: 2019_06_20-PM-02_35_53
Last ObjectModification: 2019_06_12-PM-00_25_01

Theory : num_thy_1


Home Index