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