Nuprl Definition : rclose-or-sep
rclose-or-sep(K;x;y) ==
eval x1 = (36 * K) + 1 in
if (((r1)/K x1) + 4) < (|(x - y) x1|)
then if (-((x - y) ((x1 * 20) + 1))) < ((x - y) ((x1 * 20) + 1)) then 2 else 1
else 0
Definitions occuring in Statement :
int-rdiv: (a)/k1,
rsub: x - y,
int-to-real: r(n),
absval: |i|,
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
apply: f a,
multiply: n * m,
add: n + m,
minus: -n,
natural_number: $n
FDL editor aliases :
rclose-or-sep
Latex:
rclose-or-sep(K;x;y) ==
eval x1 = (36 * K) + 1 in
if (((r1)/K x1) + 4) < (|(x - y) x1|)
then if (-((x - y) ((x1 * 20) + 1))) < ((x - y) ((x1 * 20) + 1)) then 2 else 1
else 0
Date html generated:
2020_05_20-AM-11_05_49
Last ObjectModification:
2019_11_06-PM-05_15_38
Theory : reals
Home
Index