Nuprl Definition : cover-search-right

cover-search-right(d;a;b;x) ==
  6
  * WCPR(λx.isr(d x);accelerate(3;cover-real(bool(d); a; b; x
                                             ));λk.blended-real(6 * k;cover-real(bool(d); a; b; x
                                                                                 );fst(cover-seq(bool(d);a;b;log(2;(4
                                                                                                 * 6
                                                                                                 * k)
                                                                                                 * (x + 1))
                                                                                                 + 1))))


Definitions occuring in Statement :  decdr-to-bool: bool(d),  blended-real: blended-real(k;x;y),  WCPR: WCPR(F;x;G),  cover-real: cover-real(d; a; b; cb),  cover-seq: cover-seq(d;a;b;n),  accelerate: accelerate(k;f),  log: log(b;n),  isr: isr(x),  pi1: fst(t),  apply: f a,  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  WCPR: WCPR(F;x;G),  isr: isr(x),  apply: f a,  accelerate: accelerate(k;f),  lambda: λx.A[x],  blended-real: blended-real(k;x;y),  cover-real: cover-real(d; a; b; cb),  pi1: fst(t),  cover-seq: cover-seq(d;a;b;n),  decdr-to-bool: bool(d),  log: log(b;n),  multiply: n * m,  add: n + m,  natural_number: $n
FDL editor aliases :  cover-search-right
Latex:
cover-search-right(d;a;b;x)  ==
    6
    *  WCPR(\mlambda{}x.isr(d  x);accelerate(3;cover-real(bool(d);  a;  b;  x
                                                                                          ));\mlambda{}k.blended-real(6
                                                                                                      *  k;cover-real(bool(d);  a;  b;  x
                                                                                                                                    );fst(cover-seq(bool(d);a;b;
                                                                                                                                                                    log(2;(4  *  6  *  k)
                                                                                                                                                                    *  (x  +  1))
                                                                                                                                                                    +  1))))


Date html generated: 2019_10_30-AM-07_36_51
Last ObjectModification: 2019_10_10-AM-11_35_17

Theory : reals


Home Index