Nuprl Definition : rational_fun_zero

rational_fun_zero(f;a;b) ==
  eval x = mu-ge(λn.((a (2 * n)) + 4 ≤z b (2 * n)
                    ∧b fst(ratmul(f <(a (2 * n)) + 2, 4 * n>;f <(b (2 * n)) - 2, 4 * n>)) <z 0);1) in
  eval x1 = 4 * x in
  eval x2 = (a (2 * x)) + 2 in
  eval x = (b (2 * x)) - 2 in
    let x3,x4 = f <x, x1> 
    in if (x3) < (0)  then rational-fun-zero(λx.let a,b = f x in eval a' = (-1) * a in <a', b>;<x2, x1>;<x, x1>)  else r\000Cational-fun-zero(f;<x2, x1>;<x, x1>)


Definitions occuring in Statement :  rational-fun-zero: rational-fun-zero(f;a;b),  ratmul: ratmul(a;b),  mu-ge: mu-ge(f;n),  band: p ∧b q,  callbyvalue: callbyvalue,  le_int: i ≤z j,  lt_int: i <z j,  pi1: fst(t),  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  multiply: n * m,  subtract: n - m,  add: n + m,  minus: -n,  natural_number: $n
Definitions occuring in definition :  mu-ge: mu-ge(f;n),  band: p ∧b q,  le_int: i ≤z j,  lt_int: i <z j,  pi1: fst(t),  ratmul: ratmul(a;b),  add: n + m,  subtract: n - m,  less: if (a) < (b)  then c  else d,  lambda: λx.A[x],  spread: spread def,  apply: f a,  callbyvalue: callbyvalue,  multiply: n * m,  minus: -n,  natural_number: $n,  rational-fun-zero: rational-fun-zero(f;a;b),  pair: <a, b>
FDL editor aliases :  rational_fun_zero
Latex:
rational\_fun\_zero(f;a;b)  ==
    eval  x  =  mu-ge(\mlambda{}n.((a  (2  *  n))  +  4  \mleq{}z  b  (2  *  n)
                                        \mwedge{}\msubb{}  fst(ratmul(f  <(a  (2  *  n))  +  2,  4  *  n>f  <(b  (2  *  n))  -  2,  4  *  n>))  <z  0);1)  i\000Cn
    eval  x1  =  4  *  x  in
    eval  x2  =  (a  (2  *  x))  +  2  in
    eval  x  =  (b  (2  *  x))  -  2  in
        let  x3,x4  =  f  <x,  x1> 
        in  if  (x3)  <  (0)    then  rational-fun-zero(\mlambda{}x.let  a,b  =  f  x  in  eval  a'  =  (-1)  *  a  in  <a',  b><x2,  \000Cx1><x,  x1>)    else  rational-fun-zero(f;<x2,  x1><x,  x1>)


Date html generated: 2019_10_30-AM-10_04_33
Last ObjectModification: 2019_01_14-AM-09_39_40

Theory : reals


Home Index