Nuprl Definition : add-ipoly-prepend

add-ipoly-prepend(p;q;l)
==r eval pp = p in
    eval qq = q in
      if pp = Ax then rev(l) + qq
      otherwise if qq = Ax then rev(l) + pp otherwise let p1,ps = pp

                                                      in let q1,qs = qq

                                                         in if imonomial-le(p1;q1)

                                                            then if imonomial-le(q1;p1)

                                                                 then let cp,vs = p1

                                                                      in eval c = cp + (fst(q1)) in

                                                                         eval l' = if c=0  then l  else [<c, vs> / l] in

                                                                           add-ipoly-prepend(ps;qs;l')

                                                                 else add-ipoly-prepend(ps;[q1 / qs];[p1 / l])

fi

                                                            else add-ipoly-prepend([p1 / ps];qs;[q1 / l])

fi

add-ipoly-prepend(p;q;l) ==
  fix((λadd-ipoly-prepend,p,q,l. eval pp = p in
                                 eval qq = q in
                                   if pp = Ax then rev(l) + qq
                                   otherwise if qq = Ax then rev(l) + pp
                                             otherwise let p1,ps = pp

                                                       in let q1,qs = qq

                                                          in if imonomial-le(p1;q1)

                                                             then if imonomial-le(q1;p1)

                                                                  then let cp,vs = p1

                                                                       in eval c = cp + (fst(q1)) in

                                                                          eval l' = if c=0

                                                                                       then l

                                                                                       else [<c, vs> / l] in

                                                                            add-ipoly-prepend ps qs l'

                                                                  else add-ipoly-prepend ps [q1 / qs] [p1 / l]

fi

                                                             else add-ipoly-prepend [p1 / ps] qs [q1 / l]

                                                             fi ))

  p
  q
  l

Definitions occuring in Statement : imonomial-le: imonomial-le(m1;m2), rev-append: rev(as) + bs, cons: [a / b], callbyvalue: callbyvalue, ifthenelse: if b then t else f fi , pi1: fst(t), isaxiom: if z = Ax then a otherwise b, 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 : fix: fix(F), lambda: λx.A[x], isaxiom: if z = Ax then a otherwise b, rev-append: rev(as) + bs, ifthenelse: if b then t else f fi , imonomial-le: imonomial-le(m1;m2), spread: spread def, add: n + m, pi1: fst(t), callbyvalue: callbyvalue, int_eq: if a=b then c else d, natural_number: $n, pair: <a, b>, apply: f a, cons: [a / b]
FDL editor aliases : add-ipoly-prepend

Latex:
add-ipoly-prepend(p;q;l) ==r eval pp = p in eval qq = q in if pp = Ax then rev(l) + qq otherwise if qq = Ax then rev(l) + pp otherwise let p1,ps = pp in let q1,qs = qq in if imonomial-le(p1;q1) then if imonomial-le(q1;p1) then let cp,vs = p1 in eval c = cp + (fst(q1)) in eval l' = if c=0 then l else [<c, vs> / l] in add-ipoly-prepend(ps;qs;l') else add-ipoly-prepend(ps;[q1 / qs];[p1 / l]) fi else add-ipoly-prepend([p1 / ps];qs;[q1 / l]) fi

Latex:
add-ipoly-prepend(p;q;l) == fix((\mlambda{}add-ipoly-prepend,p,q,l. eval pp = p in eval qq = q in if pp = Ax then rev(l) + qq otherwise if qq = Ax then rev(l) + pp otherwise let p1,ps = pp in let q1,qs = qq in if imonomial-le(p1;q1) then if imonomial-le(q1;p1) then let cp,vs = p1 in eval c = cp + (fst(q1)) in eval l' = if c=0 then l else [... / l] in add-ipoly-prepend ps qs l' else add-ipoly-prepend ps [q1 / qs] [p1 / l] fi else add-ipoly-prepend [p1 / ps] qs [q1 / l] fi )) p q l Date html generated: 2017_09_29-PM-05_52_47 Last ObjectModification: 2017_05_04-PM-02_58_49 Theory : omega Home Index