Nuprl Definition : i-approx

i-approx(I;n) ==
  let l,u = I 
  in case l
      of inl(x) =>
      case x
       of inl(a) =>
       case u of inl(y) => case y of inl(b) => [a, b] | inr(b) => [a, b - (r1/r(n))] | inr(y) => [a, r(n)]
       | inr(a) =>
       case u
        of inl(y) =>
        case y of inl(b) => [a + (r1/r(n)), b] | inr(b) => [a + (r1/r(n)), b - (r1/r(n))]
        | inr(y) =>
        [a + (r1/r(n)), r(n)]
      | inr(x) =>
      case u of inl(y) => case y of inl(b) => [r(-n), b] | inr(b) => [r(-n), b - (r1/r(n))] | inr(y) => [r(-n), r(n)]


Definitions occuring in Statement :  rccint: [l, u],  rdiv: (x/y),  rsub: x - y,  radd: a + b,  int-to-real: r(n),  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  minus: -n,  natural_number: $n
Definitions occuring in definition :  spread: spread def,  radd: a + b,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  rsub: x - y,  rdiv: (x/y),  natural_number: $n,  rccint: [l, u],  minus: -n,  int-to-real: r(n)
FDL editor aliases :  i-approx i-approx
Latex:
i-approx(I;n)  ==
    let  l,u  =  I 
    in  case  l
            of  inl(x)  =>
            case  x
              of  inl(a)  =>
              case  u
                of  inl(y)  =>
                case  y  of  inl(b)  =>  [a,  b]  |  inr(b)  =>  [a,  b  -  (r1/r(n))]
                |  inr(y)  =>
                [a,  r(n)]
              |  inr(a)  =>
              case  u
                of  inl(y)  =>
                case  y  of  inl(b)  =>  [a  +  (r1/r(n)),  b]  |  inr(b)  =>  [a  +  (r1/r(n)),  b  -  (r1/r(n))]
                |  inr(y)  =>
                [a  +  (r1/r(n)),  r(n)]
            |  inr(x)  =>
            case  u
              of  inl(y)  =>
              case  y  of  inl(b)  =>  [r(-n),  b]  |  inr(b)  =>  [r(-n),  b  -  (r1/r(n))]
              |  inr(y)  =>
              [r(-n),  r(n)]


Date html generated: 2016_05_18-AM-08_39_18
Last ObjectModification: 2015_09_23-AM-09_07_06

Theory : reals


Home Index