Nuprl Definition : cover-search-left
cover-search-left(d;a;b;x) ==
WCPR(λx.isl(d x);accelerate(3;cover-real(bool(d); a; b; x
));λk.blended-real(6
* k;cover-real(bool(d); a; b; x
);snd(cover-seq(bool(d);a;b;imax(log(2;(4 * 2 * 6 * k)
* (x + 1))
+ 1;log(2;(2 * 6 * k)
* (x + 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),
imax: imax(a;b),
isl: isl(x),
pi2: snd(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),
isl: isl(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),
pi2: snd(t),
cover-seq: cover-seq(d;a;b;n),
decdr-to-bool: bool(d),
imax: imax(a;b),
log: log(b;n),
multiply: n * m,
add: n + m,
natural_number: $n
FDL editor aliases :
cover-search-left
Latex:
cover-search-left(d;a;b;x) ==
WCPR(\mlambda{}x.isl(d x);accelerate(3;cover-real(bool(d); a; b; x
));\mlambda{}k.blended-real(6
* k;cover-real(bool(d); a; b; x
);snd(cover-seq(bool(d);a;b;
imax(log(2;(4
* 2
* 6
* k)
* (x + 1))
+ 1;log(2;(2
* 6
* k)
* (x + 1)))))))
Date html generated:
2019_10_30-AM-07_36_28
Last ObjectModification:
2019_10_10-AM-11_18_49
Theory : reals
Home
Index