Nuprl Definition : approx-iter-arcsine

approx-iter-arcsine(a;k;n)
==r if (n =z 0)
    then a k
    else eval m = n - 1 in
         eval k6 = 6 * k in
         eval k12 = 2 * k6 in
         eval y = approx-iter-arcsine(a;k6;m) in
           arcsine-contraction(a;(r(y))/k12) k
    fi 
approx-iter-arcsine(a;k;n) ==
  fix((λapprox-iter-arcsine,k,n. if (n =z 0)
                                then a k
                                else eval m = n - 1 in
                                     eval k6 = 6 * k in
                                     eval k12 = 2 * k6 in
                                     eval y = approx-iter-arcsine k6 m in
                                       arcsine-contraction(a;(r(y))/k12) k
                                fi )) 
  k 
  n


Definitions occuring in Statement :  arcsine-contraction: arcsine-contraction(a;x),  int-rdiv: (a)/k1,  int-to-real: r(n),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  multiply: n * m,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  int-to-real: r(n),  int-rdiv: (a)/k1,  arcsine-contraction: arcsine-contraction(a;x),  apply: f a,  callbyvalue: callbyvalue,  natural_number: $n,  multiply: n * m,  subtract: n - m,  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  fix: fix(F)
FDL editor aliases :  approx-iter-arcsine approx-iter-arcsine
Latex:
approx-iter-arcsine(a;k;n)
==r  if  (n  =\msubz{}  0)
        then  a  k
        else  eval  m  =  n  -  1  in
                  eval  k6  =  6  *  k  in
                  eval  k12  =  2  *  k6  in
                  eval  y  =  approx-iter-arcsine(a;k6;m)  in
                      arcsine-contraction(a;(r(y))/k12)  k
        fi 

Latex:
approx-iter-arcsine(a;k;n)  ==
    fix((\mlambda{}approx-iter-arcsine,k,n.  if  (n  =\msubz{}  0)
                                                                then  a  k
                                                                else  eval  m  =  n  -  1  in
                                                                          eval  k6  =  6  *  k  in
                                                                          eval  k12  =  2  *  k6  in
                                                                          eval  y  =  approx-iter-arcsine  k6  m  in
                                                                              arcsine-contraction(a;(r(y))/k12)  k
                                                                fi  )) 
    k 
    n


Date html generated: 2016_10_26-PM-00_46_02
Last ObjectModification: 2016_10_14-PM-00_11_16

Theory : reals_2


Home Index