Nuprl Definition : full-arctan
full-arctan(x) ==
case rless-case((r(-1))/2;r0;8;x)
of inl(_) =>
case rless-case((r1)/3;(r1)/2;16;x)
of inl(_) =>
case rless-case(r(2);r(3);4;x)
of inl(_) =>
2 * MachinPi4() - atan-small((r1/x))
| inr(_) =>
MachinPi4() + atan-small((x - r1/r1 + x))
| inr(_) =>
atan-small(x)
| inr(_) =>
-(case rless-case((r1)/3;(r1)/2;16;-(x))
of inl(_) =>
case rless-case(r(2);r(3);4;-(x))
of inl(_) =>
2 * MachinPi4() - atan-small((r1/-(x)))
| inr(_) =>
MachinPi4() + atan-small((-(x) - r1/r1 + -(x)))
| inr(_) =>
atan-small(-(x)))
Definitions occuring in Statement :
atan-small: atan-small(x),
MachinPi4: MachinPi4(),
rless-case: rless-case(x;y;n;z),
rdiv: (x/y),
int-rdiv: (a)/k1,
int-rmul: k1 * a,
rsub: x - y,
rminus: -(x),
radd: a + b,
int-to-real: r(n),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
minus: -n,
natural_number: $n
Definitions occuring in definition :
minus: -n,
int-rdiv: (a)/k1,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
rless-case: rless-case(x;y;n;z),
int-rmul: k1 * a,
MachinPi4: MachinPi4(),
rdiv: (x/y),
rsub: x - y,
radd: a + b,
int-to-real: r(n),
natural_number: $n,
atan-small: atan-small(x),
rminus: -(x)
FDL editor aliases :
full-arctan
Latex:
full-arctan(x) ==
case rless-case((r(-1))/2;r0;8;x)
of inl($_{}$) =>
case rless-case((r1)/3;(r1)/2;16;x)
of inl($_{}$) =>
case rless-case(r(2);r(3);4;x)
of inl($_{}$) =>
2 * MachinPi4() - atan-small((r1/x))
| inr($_{}$) =>
MachinPi4() + atan-small((x - r1/r1 + x))
| inr($_{}$) =>
atan-small(x)
| inr($_{}$) =>
-(case rless-case((r1)/3;(r1)/2;16;-(x))
of inl($_{}$) =>
case rless-case(r(2);r(3);4;-(x))
of inl($_{}$) =>
2 * MachinPi4() - atan-small((r1/-(x)))
| inr($_{}$) =>
MachinPi4() + atan-small((-(x) - r1/r1 + -(x)))
| inr($_{}$) =>
atan-small(-(x)))
Date html generated:
2018_05_22-PM-03_06_55
Last ObjectModification:
2017_10_27-AM-00_37_26
Theory : reals_2
Home
Index