Nuprl Definition : near-arcsine
near-arcsine(a;N) ==
  eval b = a 4000 in
  if (4) < (b)
     then eval b = a 400 in
          if (588) < (b)
             then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - a * a);2 * N)
             else if (b + 4) < (584)  then arcsine-approx(a;N)  else arcsine-approx(a;N)
     else if (b + 4) < (0)
             then -(eval b = -(a) 400 in
                    if (588) < (b)
                       then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - -(a) * -(a));2 * N)
                       else if (b + 4) < (584)  then arcsine-approx(-(a);N)  else arcsine-approx(-(a);N))
             else eval m = 4 * (N + 1) in
                  eval a@0 = r0 m in
                  eval b = a m in
                    if (a@0 + 4) < (b)
                       then eval b = a 400 in
                            if (588) < (b)
                               then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - a * a);2 * N)
                               else if (b + 4) < (584)  then arcsine-approx(a;N)  else arcsine-approx(a;N)
                       else if (b + 4) < (a@0)
                               then -(eval b = -(a) 400 in
                                      if (588) < (b)
                                         then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - -(a) * -(a));2 * N)
                                         else if (b + 4) < (584)
                                                 then arcsine-approx(-(a);N)
                                                 else arcsine-approx(-(a);N))
                               else r0
Definitions occuring in Statement : 
arcsine-approx: arcsine-approx(a;n)
, 
halfpi: π/2
, 
rsqrt: rsqrt(x)
, 
rational-approx: (x within 1/n)
, 
rsub: x - y
, 
rmul: a * b
, 
rminus: -(x)
, 
int-to-real: r(n)
, 
callbyvalue: callbyvalue, 
less: if (a) < (b)  then c  else d
, 
apply: f a
, 
multiply: n * m
, 
add: n + m
, 
natural_number: $n
Definitions occuring in definition : 
rminus: -(x)
, 
callbyvalue: callbyvalue, 
apply: f a
, 
rational-approx: (x within 1/n)
, 
halfpi: π/2
, 
rsqrt: rsqrt(x)
, 
rsub: x - y
, 
int-to-real: r(n)
, 
rmul: a * b
, 
multiply: n * m
, 
less: if (a) < (b)  then c  else d
, 
add: n + m
, 
natural_number: $n
, 
arcsine-approx: arcsine-approx(a;n)
FDL editor aliases : 
near-arcsine
Latex:
near-arcsine(a;N)  ==
    eval  b  =  a  4000  in
    if  (4)  <  (b)
          then  eval  b  =  a  400  in
                    if  (588)  <  (b)
                          then  (\mpi{}/2  within  1/2  *  N)  -  arcsine-approx(rsqrt(r1  -  a  *  a);2  *  N)
                          else  if  (b  +  4)  <  (584)    then  arcsine-approx(a;N)    else  arcsine-approx(a;N)
          else  if  (b  +  4)  <  (0)
                          then  -(eval  b  =  -(a)  400  in
                                        if  (588)  <  (b)
                                              then  (\mpi{}/2  within  1/2  *  N)  -  arcsine-approx(rsqrt(r1  -  -(a)  *  -(a));2  *  N)
                                              else  if  (b  +  4)  <  (584)
                                                              then  arcsine-approx(-(a);N)
                                                              else  arcsine-approx(-(a);N))
                          else  eval  m  =  4  *  (N  +  1)  in
                                    eval  a@0  =  r0  m  in
                                    eval  b  =  a  m  in
                                        if  (a@0  +  4)  <  (b)
                                              then  eval  b  =  a  400  in
                                                        if  (588)  <  (b)
                                                              then  (\mpi{}/2  within  1/2  *  N)  -  arcsine-approx(rsqrt(r1  -  a  *  a);2  *  N)
                                                              else  if  (b  +  4)  <  (584)
                                                                              then  arcsine-approx(a;N)
                                                                              else  arcsine-approx(a;N)
                                              else  if  (b  +  4)  <  (a@0)
                                                              then  -(eval  b  =  -(a)  400  in
                                                                            if  (588)  <  (b)
                                                                                  then  (\mpi{}/2  within  1/2  *  N)  -  arcsine-approx(rsqrt(r1  -  -(a)
                                                                                            *  -(a));2  *  N)
                                                                                  else  if  (b  +  4)  <  (584)
                                                                                                  then  arcsine-approx(-(a);N)
                                                                                                  else  arcsine-approx(-(a);N))
                                                              else  r0
Date html generated:
2016_10_26-PM-00_49_51
Last ObjectModification:
2016_10_13-PM-03_16_26
Theory : reals_2
Home
Index