Nuprl Definition : expr

expr(x) ==
  eval x1 = (((x 1) + 1) ÷ 2) + 1 in
  cauchy-limit(n.if n=0
                 then r0
                 else eval c = if (x1) < (0)  then 1  else 3^x1 in
                      eval nc = n * c in
                      eval m = 2 * nc in
                      eval a = (x m) - 2 in
                        (e^(r(a))/2 * m within 1/nc);λk.((2 * k) + ((2 * k) ÷ if (x1) < (0)  then 1  else 3^x1) + 1))


Definitions occuring in Statement :  rexp: e^x,  cauchy-limit: cauchy-limit(n.x[n];c),  rational-approx: (x within 1/n),  int-rdiv: (a)/k1,  int-to-real: r(n),  fastexp: i^n,  callbyvalue: callbyvalue,  less: if (a) < (b)  then c  else d,  int_eq: if a=b then c else d,  apply: f a,  lambda: λx.A[x],  divide: n ÷ m,  multiply: n * m,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  cauchy-limit: cauchy-limit(n.x[n];c),  int_eq: if a=b then c else d,  callbyvalue: callbyvalue,  subtract: n - m,  apply: f a,  rational-approx: (x within 1/n),  rexp: e^x,  int-rdiv: (a)/k1,  int-to-real: r(n),  lambda: λx.A[x],  add: n + m,  divide: n ÷ m,  multiply: n * m,  less: if (a) < (b)  then c  else d,  fastexp: i^n,  natural_number: $n
FDL editor aliases :  expr
Latex:
expr(x)  ==
    eval  x1  =  (((x  1)  +  1)  \mdiv{}  2)  +  1  in
    cauchy-limit(n.if  n=0
                                  then  r0
                                  else  eval  c  =  if  (x1)  <  (0)    then  1    else  3\^{}x1  in
                                            eval  nc  =  n  *  c  in
                                            eval  m  =  2  *  nc  in
                                            eval  a  =  (x  m)  -  2  in
                                                (e\^{}(r(a))/2  *  m  within  1/nc);\mlambda{}k.((2  *  k)
                                                                                                                +  ((2  *  k)  \mdiv{}  if  (x1)  <  (0)
                                                                                                                                                then  1
                                                                                                                                                else  3\^{}x1)
                                                                                                                +  1))


Date html generated: 2019_10_31-AM-06_11_27
Last ObjectModification: 2019_01_30-PM-02_42_39

Theory : reals_2


Home Index