`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)`
Latex:
==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)
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:
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