Nuprl Definition : rat_term_to_real

rat_term_to_real(f;t) ==
  rat_term_ind(t;
               rtermConstant(n)⇒ <True, r(n)>;
               rtermVar(v)⇒ <True, f v>;
               rtermAdd(left,right)⇒ rl,rr.let P,x = rl 
                                            in let Q,y = rr 
                                               in <P ∧ Q, x + y>;
               rtermSubtract(left,right)⇒ rl,rr.let P,x = rl 
                                                 in let Q,y = rr 
                                                    in <P ∧ Q, x - y>;
               rtermMultiply(left,right)⇒ rl,rr.let P,x = rl 
                                                 in let Q,y = rr 
                                                    in <P ∧ Q, x * y>;
               rtermDivide(num,denom)⇒ rl,rr.let P,x = rl 
                                              in let Q,y = rr 
                                                 in <(P ∧ Q) ∧ y ≠ r0, (x/y)>;
               rtermMinus(num)⇒ rx.let P,x = rx 
                                    in <P, -(x)>) 


Definitions occuring in Statement :  rdiv: (x/y),  rneq: x ≠ y,  rat_term_ind: rat_term_ind,  rsub: x - y,  rmul: a * b,  rminus: -(x),  radd: a + b,  int-to-real: r(n),  and: P ∧ Q,  true: True,  apply: f a,  spread: spread def,  pair: <a, b>,  natural_number: $n
Definitions occuring in definition :  rat_term_ind: rat_term_ind,  true: True,  apply: f a,  radd: a + b,  rsub: x - y,  rmul: a * b,  and: P ∧ Q,  int-to-real: r(n),  natural_number: $n,  spread: spread def,  pair: <a, b>,  rminus: -(x)
FDL editor aliases :  rat_term_to_real
Latex:
rat\_term\_to\_real(f;t)  ==
    rat\_term\_ind(t;
                              rtermConstant(n){}\mRightarrow{}  <True,  r(n)>
                              rtermVar(v){}\mRightarrow{}  <True,  f  v>
                              rtermAdd(left,right){}\mRightarrow{}  rl,rr.let  P,x  =  rl 
                                                                                        in  let  Q,y  =  rr 
                                                                                              in  <P  \mwedge{}  Q,  x  +  y>
                              rtermSubtract(left,right){}\mRightarrow{}  rl,rr.let  P,x  =  rl 
                                                                                                  in  let  Q,y  =  rr 
                                                                                                        in  <P  \mwedge{}  Q,  x  -  y>
                              rtermMultiply(left,right){}\mRightarrow{}  rl,rr.let  P,x  =  rl 
                                                                                                  in  let  Q,y  =  rr 
                                                                                                        in  <P  \mwedge{}  Q,  x  *  y>
                              rtermDivide(num,denom){}\mRightarrow{}  rl,rr.let  P,x  =  rl 
                                                                                            in  let  Q,y  =  rr 
                                                                                                  in  <(P  \mwedge{}  Q)  \mwedge{}  y  \mneq{}  r0,  (x/y)>
                              rtermMinus(num){}\mRightarrow{}  rx.let  P,x  =  rx 
                                                                        in  <P,  -(x)>) 


Date html generated: 2019_10_29-AM-09_40_22
Last ObjectModification: 2019_04_01-AM-00_04_33

Theory : reals


Home Index