Nuprl Definition : rat_term_to_ipolys

rat_term_to_ipolys(t) ==
  rat_term_ind(t;
               rtermConstant(c)⇒ <if c=0 then [] else [<c, []>], [<1, []>]>;
               rtermVar(v)⇒ <[<1, [v]>], [<1, []>]>;
               rtermAdd(left,right)⇒ rl,rr.let p1,q1 = rl 
                                            in let p2,q2 = rr 
                                               in <add_ipoly(mul_ipoly(p1;q2);mul_ipoly(p2;q1)), mul_ipoly(q1;q2)>;
               rtermSubtract(left,right)⇒ rl,rr.let p1,q1 = rl 
                                                 in let p2,q2 = rr 
                                                    in <add_ipoly(mul_ipoly(p1;q2);mul_ipoly(minus-poly(p2);q1))
                                                       , mul_ipoly(q1;q2)
                                                       >;
               rtermMultiply(left,right)⇒ rl,rr.let p1,q1 = rl 
                                                 in let p2,q2 = rr 
                                                    in <mul_ipoly(p1;p2), mul_ipoly(q1;q2)>;
               rtermDivide(num,denom)⇒ rl,rr.let p1,q1 = rl 
                                              in let p2,q2 = rr 
                                                 in <mul_ipoly(p1;q2), mul_ipoly(q1;p2)>;
               rtermMinus(num)⇒ rx.let p1,q1 = rx 
                                    in <minus-poly(p1), q1>) 


Definitions occuring in Statement :  rat_term_ind: rat_term_ind,  mul_ipoly: mul_ipoly(p;q),  minus-poly: minus-poly(p),  add_ipoly: add_ipoly(p;q),  cons: [a / b],  nil: [],  int_eq: if a=b then c else d,  spread: spread def,  pair: <a, b>,  natural_number: $n
Definitions occuring in definition :  rat_term_ind: rat_term_ind,  int_eq: if a=b then c else d,  cons: [a / b],  natural_number: $n,  nil: [],  add_ipoly: add_ipoly(p;q),  mul_ipoly: mul_ipoly(p;q),  spread: spread def,  pair: <a, b>,  minus-poly: minus-poly(p)
FDL editor aliases :  rat_term_to_ipolys
Latex:
rat\_term\_to\_ipolys(t)  ==
    rat\_term\_ind(t;
                              rtermConstant(c){}\mRightarrow{}  <if  c=0  then  []  else  [<c,  []>],  [ə,  []>]>
                              rtermVar(v){}\mRightarrow{}  <[ə,  [v]>],  [ə,  []>]>
                              rtermAdd(left,right){}\mRightarrow{}  rl,rr.let  p1,q1  =  rl 
                                                                                        in  let  p2,q2  =  rr 
                                                                                              in  <add\_ipoly(mul\_ipoly(p1;q2);mul\_ipoly(p2;q1))
                                                                                                    ,  mul\_ipoly(q1;q2)
                                                                                                    >
                              rtermSubtract(left,right){}\mRightarrow{}  rl,rr.let  p1,q1  =  rl 
                                                                                                  in  let  p2,q2  =  rr 
                                                                                                        in  <add\_ipoly(mul\_ipoly(p1;q2);...)
                                                                                                              ,  mul\_ipoly(q1;q2)
                                                                                                              >
                              rtermMultiply(left,right){}\mRightarrow{}  rl,rr.let  p1,q1  =  rl 
                                                                                                  in  let  p2,q2  =  rr 
                                                                                                        in  <mul\_ipoly(p1;p2),  mul\_ipoly(q1;q2)>
                              rtermDivide(num,denom){}\mRightarrow{}  rl,rr.let  p1,q1  =  rl 
                                                                                            in  let  p2,q2  =  rr 
                                                                                                  in  <mul\_ipoly(p1;q2),  mul\_ipoly(q1;p2)>
                              rtermMinus(num){}\mRightarrow{}  rx.let  p1,q1  =  rx 
                                                                        in  <minus-poly(p1),  q1>) 


Date html generated: 2019_10_29-AM-09_31_19
Last ObjectModification: 2019_04_01-PM-00_38_28

Theory : reals


Home Index