Nuprl Definition : rsine
rsine(x) ==
eval n = reduce-halfpi(x) in
eval i = n mod 4 in
if (i =z 0) then sine-medium(x - n * 2 * MachinPi4())
if (i =z 2) then -(sine-medium(x - n * 2 * MachinPi4()))
if (i =z 1) then cosine-medium(x - n * 2 * MachinPi4())
else -(cosine-medium(x - n * 2 * MachinPi4()))
fi
Definitions occuring in Statement :
reduce-halfpi: reduce-halfpi(x),
MachinPi4: MachinPi4(),
cosine-medium: cosine-medium(x),
sine-medium: sine-medium(x),
int-rmul: k1 * a,
rsub: x - y,
rminus: -(x),
modulus: a mod n,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n
Definitions occuring in definition :
reduce-halfpi: reduce-halfpi(x),
callbyvalue: callbyvalue,
modulus: a mod n,
sine-medium: sine-medium(x),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
rminus: -(x),
cosine-medium: cosine-medium(x),
rsub: x - y,
int-rmul: k1 * a,
natural_number: $n,
MachinPi4: MachinPi4()
FDL editor aliases :
rsine
Latex:
rsine(x) ==
eval n = reduce-halfpi(x) in
eval i = n mod 4 in
if (i =\msubz{} 0) then sine-medium(x - n * 2 * MachinPi4())
if (i =\msubz{} 2) then -(sine-medium(x - n * 2 * MachinPi4()))
if (i =\msubz{} 1) then cosine-medium(x - n * 2 * MachinPi4())
else -(cosine-medium(x - n * 2 * MachinPi4()))
fi
Date html generated:
2019_10_31-AM-06_07_19
Last ObjectModification:
2019_02_03-PM-07_59_18
Theory : reals_2
Home
Index