Nuprl Definition : rnexp
x^k1 ==
eval k = k1 in
if (k =z 0)
then r1
else eval B = canon-bnd(x) in
accelerate((k * ((B^k - 1 ÷ 2^k - 1) + 1)) + 1;λn.(x n^k ÷ 2 * n^k - 1))
fi
Definitions occuring in Statement :
canon-bnd: canon-bnd(x),
int-to-real: r(n),
accelerate: accelerate(k;f),
fastexp: i^n,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
divide: n ÷ m,
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
int-to-real: r(n),
callbyvalue: callbyvalue,
canon-bnd: canon-bnd(x),
accelerate: accelerate(k;f),
add: n + m,
lambda: λx.A[x],
divide: n ÷ m,
apply: f a,
fastexp: i^n,
multiply: n * m,
subtract: n - m,
natural_number: $n
FDL editor aliases :
rnexp
rnexp
Latex:
x\^{}k1 ==
eval k = k1 in
if (k =\msubz{} 0)
then r1
else eval B = canon-bnd(x) in
accelerate((k * ((B\^{}k - 1 \mdiv{} 2\^{}k - 1) + 1)) + 1;\mlambda{}n.(x n\^{}k \mdiv{} 2 * n\^{}k - 1))
fi
Date html generated:
2019_10_29-AM-09_33_54
Last ObjectModification:
2019_01_31-PM-08_04_32
Theory : reals
Home
Index