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:
add-polynom(n;rmz;p;q)
==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:
add-polynom(n;rmz;p;q)  ==
    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