Nuprl Definition : int_term_to_ipoly

int_term_to_ipoly(t) ==
  int_term_ind(t;
               itermConstant(c)⇒ if c=0  then []  else [<c, []>];
               itermVar(v)⇒ [<1, [v]>];
               itermAdd(l,r)⇒ rl,rr.add_ipoly(rl;rr);
               itermSubtract(l,r)⇒ rl,rr.add_ipoly(rl;minus-poly(rr));
               itermMultiply(l,r)⇒ rl,rr.mul_ipoly(rl;rr);
               itermMinus(x)⇒ rx.minus-poly(rx)) 


Definitions occuring in Statement :  mul_ipoly: mul_ipoly(p;q),  minus-poly: minus-poly(p),  add_ipoly: add_ipoly(p;q),  int_term_ind: int_term_ind,  cons: [a / b],  nil: [],  int_eq: if a=b  then c  else d,  pair: <a, b>,  natural_number: $n
Definitions occuring in definition :  int_term_ind: int_term_ind,  int_eq: if a=b  then c  else d,  pair: <a, b>,  natural_number: $n,  cons: [a / b],  nil: [],  add_ipoly: add_ipoly(p;q),  mul_ipoly: mul_ipoly(p;q),  minus-poly: minus-poly(p)
FDL editor aliases :  int_term_to_ipoly
Latex:
int\_term\_to\_ipoly(t)  ==
    int\_term\_ind(t;
                              itermConstant(c){}\mRightarrow{}  if  c=0    then  []    else  [<c,  []>];
                              itermVar(v){}\mRightarrow{}  [ə,  [v]>];
                              itermAdd(l,r){}\mRightarrow{}  rl,rr.add\_ipoly(rl;rr);
                              itermSubtract(l,r){}\mRightarrow{}  rl,rr.add\_ipoly(rl;minus-poly(rr));
                              itermMultiply(l,r){}\mRightarrow{}  rl,rr.mul\_ipoly(rl;rr);
                              itermMinus(x){}\mRightarrow{}  rx.minus-poly(rx)) 


Date html generated: 2017_09_29-PM-05_54_33
Last ObjectModification: 2017_05_04-PM-05_51_52

Theory : omega


Home Index