Nuprl Definition : find_rational

find_rational(a;b;d) ==
  if d b then b
  if d a then a
  else let x,n =
        find-ge-val(λx.isl(x);λn.case int_seg_decide(λk.(d 
                                                         ratreduce(rat-nat-div(ratadd(int-rat-mul(k;a);int-rat-mul(n 
                                                         - k;b));n)));1;n)
                                  of inl(p) =>
                                  inl (fst(p))
                                  | inr(_) =>
                                  inr Ax ;2) 
       in case x
           of inl(y) =>
           eval k = y in
           ratreduce(rat-nat-div(ratadd(int-rat-mul(k;a);int-rat-mul(n - k;b));n))
           | inr(y) =>
           eval k = fix((λx.x)) in
           ratreduce(rat-nat-div(ratadd(int-rat-mul(k;a);int-rat-mul(n - k;b));n))
  fi 


Definitions occuring in Statement :  rat-nat-div: rat-nat-div(x;n),  int-rat-mul: int-rat-mul(n;x),  ratreduce: ratreduce(x),  ratadd: ratadd(x;y),  find-ge-val: find-ge-val(test;f;n),  int_seg_decide: int_seg_decide(d;i;j),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  isl: isl(x),  pi1: fst(t),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  subtract: n - m,  natural_number: $n,  axiom: Ax
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  spread: spread def,  find-ge-val: find-ge-val(test;f;n),  isl: isl(x),  int_seg_decide: int_seg_decide(d;i;j),  apply: f a,  inl: inl x,  pi1: fst(t),  inr: inr x ,  axiom: Ax,  natural_number: $n,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  callbyvalue: callbyvalue,  fix: fix(F),  lambda: λx.A[x],  ratreduce: ratreduce(x),  rat-nat-div: rat-nat-div(x;n),  ratadd: ratadd(x;y),  int-rat-mul: int-rat-mul(n;x),  subtract: n - m
FDL editor aliases :  find_rational
Latex:
find\_rational(a;b;d)  ==
    if  d  b
        then  b
    if  d  a
        then  a
    else  let  x,n  =
                find-ge-val(\mlambda{}x.isl(x);\mlambda{}n.case  int\_seg\_decide(...;1;n)
                                                                    of  inl(p)  =>
                                                                    inl  (fst(p))
                                                                    |  inr($_{}$)  =>
                                                                    inr  Ax  ;2) 
              in  case  x
                      of  inl(y)  =>
                      eval  k  =  y  in
                      ratreduce(rat-nat-div(ratadd(int-rat-mul(k;a);int-rat-mul(n  -  k;b));n))
                      |  inr(y)  =>
                      eval  k  =  fix((\mlambda{}x.x))  in
                      ratreduce(rat-nat-div(ratadd(int-rat-mul(k;a);int-rat-mul(n  -  k;b));n))
    fi 


Date html generated: 2019_10_30-AM-10_08_03
Last ObjectModification: 2019_01_20-PM-00_43_00

Theory : reals


Home Index