Nuprl Definition : cover-seq

cover-seq(d;a;b;n) ==
  primrec(n;<a, b>;λi,p. let a,b = p in case d (a + b/r(2)) of inl(z) => <(a + b/r(2)), b> | inr(z) => <a, (a + b/r(2))>\000C)


Definitions occuring in Statement :  rdiv: (x/y),  radd: a + b,  int-to-real: r(n),  primrec: primrec(n;b;c),  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  natural_number: $n
Definitions occuring in definition :  primrec: primrec(n;b;c),  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply: f a,  pair: <a, b>,  rdiv: (x/y),  radd: a + b,  int-to-real: r(n),  natural_number: $n
FDL editor aliases :  cover-seq
Latex:
cover-seq(d;a;b;n)  ==
    primrec(n;<a,  b>\mlambda{}i,p.  let  a,b  =  p 
                                              in  case  d  (a  +  b/r(2))
                                                      of  inl(z)  =>
                                                      <(a  +  b/r(2)),  b>
                                                      |  inr(z)  =>
                                                      <a,  (a  +  b/r(2))>)


Date html generated: 2017_10_03-AM-10_02_34
Last ObjectModification: 2017_07_06-AM-10_49_24

Theory : reals


Home Index