Nuprl Definition : altered-seq1
altered-seq1(d; a; b; x; n) == blended-real(6 * cover-search-left(d;a;b;x);cover-real(bool(d); a; b; x);n)
Definitions occuring in Statement :
cover-search-left: cover-search-left(d;a;b;x),
decdr-to-bool: bool(d),
blended-real: blended-real(k;x;y),
cover-real: cover-real(d; a; b; cb),
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
decdr-to-bool: bool(d),
cover-real: cover-real(d; a; b; cb),
cover-search-left: cover-search-left(d;a;b;x),
natural_number: $n,
multiply: n * m,
blended-real: blended-real(k;x;y)
Latex:
altered-seq1(d; a; b; x; n) ==
blended-real(6 * cover-search-left(d;a;b;x);cover-real(bool(d); a; b; x);n)
Date html generated:
2017_10_03-AM-10_17_25
Last ObjectModification:
2017_09_20-PM-07_01_08
Theory : reals
Home
Index