Nuprl Definition : full-arcsin
full-arcsin(a) ==
case rless-case((r(73))/100;(r(3))/4;110;|a|)
of inl(u) =>
case rless-case(r0;(r1)/2;10;a)
of inl(u) =>
2 * MachinPi4() - partial-arcsin(rsqrt(r1 - a * a))
| inr(v) =>
partial-arcsin(rsqrt(r1 - a * a)) - 2 * MachinPi4()
| inr(v) =>
partial-arcsin(a)
Definitions occuring in Statement :
partial-arcsin: partial-arcsin(a),
MachinPi4: MachinPi4(),
rsqrt: rsqrt(x),
rless-case: rless-case(x;y;n;z),
rabs: |x|,
int-rdiv: (a)/k1,
int-rmul: k1 * a,
rsub: x - y,
rmul: a * b,
int-to-real: r(n),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n
Definitions occuring in definition :
rabs: |x|,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
rless-case: rless-case(x;y;n;z),
int-rdiv: (a)/k1,
rsqrt: rsqrt(x),
rsub: x - y,
int-to-real: r(n),
rmul: a * b,
int-rmul: k1 * a,
natural_number: $n,
MachinPi4: MachinPi4(),
partial-arcsin: partial-arcsin(a)
FDL editor aliases :
full-arcsin
Latex:
full-arcsin(a) ==
case rless-case((r(73))/100;(r(3))/4;110;|a|)
of inl(u) =>
case rless-case(r0;(r1)/2;10;a)
of inl(u) =>
2 * MachinPi4() - partial-arcsin(rsqrt(r1 - a * a))
| inr(v) =>
partial-arcsin(rsqrt(r1 - a * a)) - 2 * MachinPi4()
| inr(v) =>
partial-arcsin(a)
Date html generated:
2019_10_31-AM-06_13_30
Last ObjectModification:
2019_05_21-PM-05_27_11
Theory : reals_2
Home
Index