Nuprl Definition : rational-fun-zero

rational-fun-zero(f;a;b) ==
  λn.eval m = 4 * n in
     (ratreal(fst(primrec(exp-ratio(1;2;0;ratbound(ratsub(b;a)) * m;1);<a, b>;λi,p. let x,y = p 
                                       in eval m = rat-nat-div(ratadd(x;y);2) in
                                          eval r = f m in
                                            let x1,x2 = r 
                                            in if (x1) < (0)  then <m, y>  else <x, m>))) 
      m) ÷ 4


Definitions occuring in Statement :  ratbound: ratbound(x),  rat-nat-div: rat-nat-div(x;n),  ratsub: ratsub(x;y),  ratadd: ratadd(x;y),  ratreal: ratreal(r),  exp-ratio: exp-ratio(a;b;n;p;q),  primrec: primrec(n;b;c),  callbyvalue: callbyvalue,  pi1: fst(t),  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  divide: n ÷ m,  multiply: n * m,  natural_number: $n
Definitions occuring in definition :  divide: n ÷ m,  ratreal: ratreal(r),  pi1: fst(t),  primrec: primrec(n;b;c),  exp-ratio: exp-ratio(a;b;n;p;q),  multiply: n * m,  ratbound: ratbound(x),  ratsub: ratsub(x;y),  lambda: λx.A[x],  rat-nat-div: rat-nat-div(x;n),  ratadd: ratadd(x;y),  callbyvalue: callbyvalue,  apply: f a,  spread: spread def,  less: if (a) < (b)  then c  else d,  pair: <a, b>,  natural_number: $n
FDL editor aliases :  rational-fun-zero
Latex:
rational-fun-zero(f;a;b)  ==
    \mlambda{}n.eval  m  =  4  *  n  in
          (ratreal(fst(primrec(exp-ratio(1;2;0;ratbound(ratsub(b;a))  *  m;1);<a,  b>\mlambda{}i,p.  let  x,y  =  p 
                                                                              in  eval  m  =  rat-nat-div(ratadd(x;y);2)  in
                                                                                    eval  r  =  f  m  in
                                                                                        let  x1,x2  =  r 
                                                                                        in  if  (x1)  <  (0)    then  <m,  y>    else  <x,  m>))) 
            m)  \mdiv{}  4


Date html generated: 2019_10_30-AM-10_00_48
Last ObjectModification: 2019_01_11-PM-03_42_09

Theory : reals


Home Index