Nuprl Definition : logseq

logseq(a;b;n) ==
  primrec(n;b;λi,x. eval j = i + 1 in
                    eval N = 4 * 10^3^j in
                    eval xx = x N in
                    eval N2 = 2 * N in
                      (lgc(a;(r(xx))/N2) within 1/N))


Definitions occuring in Statement :  lgc: lgc(a;x),  rational-approx: (x within 1/n),  int-rdiv: (a)/k1,  int-to-real: r(n),  fastexp: i^n,  primrec: primrec(n;b;c),  callbyvalue: callbyvalue,  apply: f a,  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  primrec: primrec(n;b;c),  lambda: λx.A[x],  add: n + m,  fastexp: i^n,  apply: f a,  callbyvalue: callbyvalue,  multiply: n * m,  natural_number: $n,  rational-approx: (x within 1/n),  lgc: lgc(a;x),  int-rdiv: (a)/k1,  int-to-real: r(n)
FDL editor aliases :  logseq
Latex:
logseq(a;b;n)  ==
    primrec(n;b;\mlambda{}i,x.  eval  j  =  i  +  1  in
                                        eval  N  =  4  *  10\^{}3\^{}j  in
                                        eval  xx  =  x  N  in
                                        eval  N2  =  2  *  N  in
                                            (lgc(a;(r(xx))/N2)  within  1/N))


Date html generated: 2019_10_31-AM-06_09_03
Last ObjectModification: 2019_01_28-PM-07_31_01

Theory : reals_2


Home Index