Nuprl Definition : add-ipoly

add-ipoly(p;q)
==r eval pp = p in
    eval qq = q in
      if null(pp) then qq
      if null(qq) then pp
      else let p1,ps = pp 
           in let q1,qs = qq 
              in if imonomial-le(p1;q1)
                 then if imonomial-le(q1;p1)
                      then let x ⟵ add-ipoly(ps;qs)
                           in let cp,vs = p1 
                              in eval c = cp + (fst(q1)) in
                                 if c=0  then x  else [<c, vs> / x]
                      else let x ⟵ add-ipoly(ps;[q1 / qs])
                           in [p1 / x]
                      fi 
                 else let x ⟵ add-ipoly([p1 / ps];qs)
                      in [q1 / x]
                 fi 
      fi 
add-ipoly(p;q) ==
  fix((λadd-ipoly,p,q. eval pp = p in
                       eval qq = q in
                         if null(pp) then qq
                         if null(qq) then pp
                         else let p1,ps = pp 
                              in let q1,qs = qq 
                                 in if imonomial-le(p1;q1)
                                    then if imonomial-le(q1;p1)
                                         then let x ⟵ add-ipoly ps qs
                                              in let cp,vs = p1 
                                                 in eval c = cp + (fst(q1)) in
                                                    if c=0  then x  else [<c, vs> / x]
                                         else let x ⟵ add-ipoly ps [q1 / qs]
                                              in [p1 / x]
                                         fi 
                                    else let x ⟵ add-ipoly [p1 / ps] qs
                                         in [q1 / x]
                                    fi 
                         fi )) 
  p 
  q


Definitions occuring in Statement :  imonomial-le: imonomial-le(m1;m2),  null: null(as),  cons: [a / b],  callbyvalueall: callbyvalueall,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  pi1: fst(t),  int_eq: if a=b  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n
Definitions occuring in definition :  cons: [a / b],  apply: f a,  callbyvalueall: callbyvalueall,  pair: <a, b>,  natural_number: $n,  int_eq: if a=b  then c  else d,  pi1: fst(t),  add: n + m,  callbyvalue: callbyvalue,  spread: spread def,  imonomial-le: imonomial-le(m1;m2),  ifthenelse: if b then t else f fi ,  null: null(as),  lambda: λx.A[x],  fix: fix(F)
FDL editor aliases :  add-ipoly add-ipoly add-ipoly
Latex:
add-ipoly(p;q)
==r  eval  pp  =  p  in
        eval  qq  =  q  in
            if  null(pp)  then  qq
            if  null(qq)  then  pp
            else  let  p1,ps  =  pp 
                      in  let  q1,qs  =  qq 
                            in  if  imonomial-le(p1;q1)
                                  then  if  imonomial-le(q1;p1)
                                            then  let  x  \mleftarrow{}{}  add-ipoly(ps;qs)
                                                      in  let  cp,vs  =  p1 
                                                            in  eval  c  =  cp  +  (fst(q1))  in
                                                                  if  c=0    then  x    else  [<c,  vs>  /  x]
                                            else  let  x  \mleftarrow{}{}  add-ipoly(ps;[q1  /  qs])
                                                      in  [p1  /  x]
                                            fi 
                                  else  let  x  \mleftarrow{}{}  add-ipoly([p1  /  ps];qs)
                                            in  [q1  /  x]
                                  fi 
            fi 

Latex:
add-ipoly(p;q)  ==
    fix((\mlambda{}add-ipoly,p,q.  eval  pp  =  p  in
                                              eval  qq  =  q  in
                                                  if  null(pp)  then  qq
                                                  if  null(qq)  then  pp
                                                  else  let  p1,ps  =  pp 
                                                            in  let  q1,qs  =  qq 
                                                                  in  if  imonomial-le(p1;q1)
                                                                        then  if  imonomial-le(q1;p1)
                                                                                  then  let  x  \mleftarrow{}{}  add-ipoly  ps  qs
                                                                                            in  let  cp,vs  =  p1 
                                                                                                  in  eval  c  =  cp  +  (fst(q1))  in
                                                                                                        if  c=0    then  x    else  [<c,  vs>  /  x]
                                                                                  else  let  x  \mleftarrow{}{}  add-ipoly  ps  [q1  /  qs]
                                                                                            in  [p1  /  x]
                                                                                  fi 
                                                                        else  let  x  \mleftarrow{}{}  add-ipoly  [p1  /  ps]  qs
                                                                                  in  [q1  /  x]
                                                                        fi 
                                                  fi  )) 
    p 
    q


Date html generated: 2017_04_14-AM-08_58_03
Last ObjectModification: 2017_04_12-PM-06_35_38

Theory : omega


Home Index