### Nuprl Definition : add-polynom

`add-polynom(n;rmz;p;q)`
`==r if (n =z 0)`
`    then p + q`
`    else let pp ⟵ p`
`         in let qq ⟵ q`
`            in if null(pp) then qq`
`            if null(qq) then pp`
`            else eval m = ||pp|| in`
`                 eval k = ||qq|| in`
`                   if (m) < (k)`
`                      then let b,bs = qq `
`                           in let cs ⟵ add-polynom(n;ff;pp;bs)`
`                              in [b / cs]`
`                      else if (k) < (m)`
`                              then let a,as = pp `
`                                   in let cs ⟵ add-polynom(n;ff;as;qq)`
`                                      in [a / cs]`
`                              else let a,as = p `
`                                   in let b,bs = q `
`                                      in let c ⟵ add-polynom(n - 1;tt;a;b)`
`                                         in let cs ⟵ add-polynom(n;ff;as;bs)`
`                                            in if rmz then rm-zeros(n - 1;[c / cs]) else [c / cs] fi `
`            fi `
`    fi `

`add-polynom(n;rmz;p;q) ==`
`  fix((λadd-polynom,n,rmz,p,q. if (n =z 0)`
`                              then p + q`
`                              else let pp ⟵ p`
`                                   in let qq ⟵ q`
`                                      in if null(pp) then qq`
`                                      if null(qq) then pp`
`                                      else eval m = ||pp|| in`
`                                           eval k = ||qq|| in`
`                                             if (m) < (k)`
`                                                then let b,bs = qq `
`                                                     in let cs ⟵ add-polynom n ff pp bs`
`                                                        in [b / cs]`
`                                                else if (k) < (m)`
`                                                        then let a,as = pp `
`                                                             in let cs ⟵ add-polynom n ff as qq`
`                                                                in [a / cs]`
`                                                        else let a,as = p `
`                                                             in let b,bs = q `
`                                                                in let c ⟵ add-polynom (n - 1) tt a b`
`                                                                   in let cs ⟵ add-polynom n ff as bs`
`                                                                      in if rmz`
`                                                                      then rm-zeros(n - 1;[c / cs])`
`                                                                      else [c / cs]`
`                                                                      fi `
`                                      fi `
`                              fi )) `
`  n `
`  rmz `
`  p `
`  q`

Definitions occuring in Statement :  rm-zeros: `rm-zeros(n;p)` length: `||as||` null: `null(as)` cons: `[a / b]` callbyvalueall: callbyvalueall callbyvalue: callbyvalue ifthenelse: `if b then t else f fi ` eq_int: `(i =z j)` bfalse: `ff` btrue: `tt` less: `if (a) < (b)  then c  else d` apply: `f a` fix: `fix(F)` lambda: `λx.A[x]` spread: spread def subtract: `n - m` add: `n + m` natural_number: `\$n`
Definitions occuring in definition :  fix: `fix(F)` lambda: `λx.A[x]` eq_int: `(i =z j)` add: `n + m` null: `null(as)` callbyvalue: callbyvalue length: `||as||` less: `if (a) < (b)  then c  else d` spread: spread def btrue: `tt` callbyvalueall: callbyvalueall apply: `f a` bfalse: `ff` ifthenelse: `if b then t else f fi ` rm-zeros: `rm-zeros(n;p)` subtract: `n - m` natural_number: `\$n` cons: `[a / b]`
FDL editor aliases :  add-polynom
Latex:
==r  if  (n  =\msubz{}  0)
then  p  +  q
else  let  pp  \mleftarrow{}{}  p
in  let  qq  \mleftarrow{}{}  q
in  if  null(pp)  then  qq
if  null(qq)  then  pp
else  eval  m  =  ||pp||  in
eval  k  =  ||qq||  in
if  (m)  <  (k)
then  let  b,bs  =  qq
in  let  cs  \mleftarrow{}{}  add-polynom(n;ff;pp;bs)
in  [b  /  cs]
else  if  (k)  <  (m)
then  let  a,as  =  pp
in  let  cs  \mleftarrow{}{}  add-polynom(n;ff;as;qq)
in  [a  /  cs]
else  let  a,as  =  p
in  let  b,bs  =  q
in  let  c  \mleftarrow{}{}  add-polynom(n  -  1;tt;a;b)
in  let  cs  \mleftarrow{}{}  add-polynom(n;ff;as;bs)
in  if  rmz
then  rm-zeros(n  -  1;[c  /  cs])
else  [c  /  cs]
fi
fi
fi

Latex:
fix((\mlambda{}add-polynom,n,rmz,p,q.  if  (n  =\msubz{}  0)
then  p  +  q
else  let  pp  \mleftarrow{}{}  p
in  let  qq  \mleftarrow{}{}  q
in  if  null(pp)  then  qq
if  null(qq)  then  pp
else  eval  m  =  ||pp||  in
eval  k  =  ||qq||  in
if  (m)  <  (k)
then  let  b,bs  =  qq
in  let  cs  \mleftarrow{}{}  add-polynom  n  ff  pp  bs
in  [b  /  cs]
else  if  (k)  <  (m)
then  let  a,as  =  pp
in  let  cs  \mleftarrow{}{}  add-polynom  n  ff  as  qq
in  [a  /  cs]
else  let  a,as  =  p
in  let  b,bs  =  q
in  let  c  \mleftarrow{}{}  add-polynom  (n  -  1)  tt
a
b
in  let  cs  \mleftarrow{}{}  add-polynom  n  ff  as
bs
in  if  rmz
then  rm-zeros(n  -  1;[c  /  cs])
else  [c  /  cs]
fi
fi
fi  ))
n
rmz
p
q

Date html generated: 2017_09_29-PM-05_59_52
Last ObjectModification: 2017_04_26-PM-02_04_44

Theory : integer!polynomials

Home Index