Nuprl Definition : rational-inner-approx
rational-inner-approx(x;n) ==
  eval m = 2 * n in
  eval z = x m in
  eval a = if 4 <z z then z - 2
           if z <z -4 then z + 2
           else 0
           fi  in
    (r(a))/2 * m
Definitions occuring in Statement : 
int-rdiv: (a)/k1, 
int-to-real: r(n), 
callbyvalue: callbyvalue, 
ifthenelse: if b then t else f fi , 
lt_int: i <z j, 
apply: f a, 
multiply: n * m, 
subtract: n - m, 
add: n + m, 
minus: -n, 
natural_number: $n
Definitions occuring in definition : 
apply: f a, 
callbyvalue: callbyvalue, 
subtract: n - m, 
ifthenelse: if b then t else f fi , 
lt_int: i <z j, 
minus: -n, 
add: n + m, 
int-rdiv: (a)/k1, 
int-to-real: r(n), 
multiply: n * m, 
natural_number: $n
FDL editor aliases : 
rational-inner-approx
Latex:
rational-inner-approx(x;n)  ==
    eval  m  =  2  *  n  in
    eval  z  =  x  m  in
    eval  a  =  if  4  <z  z  then  z  -  2
                      if  z  <z  -4  then  z  +  2
                      else  0
                      fi    in
        (r(a))/2  *  m
Date html generated:
2019_10_29-AM-10_02_08
Last ObjectModification:
2019_06_17-PM-02_24_09
Theory : reals
Home
Index