Nuprl Definition : add-polyn
add-polyn(n;p;q)
==r if (n =z 0)
    then p + q
    else if p = Ax then q
         otherwise if q = Ax then p otherwise eval rp = rev(p) in
                                              eval rq = rev(q) in
                                              eval cs = list_accum2(sofar,a,b.eval c = add-polyn(n - 1;a;b) in
                                                                              [c / sofar];sofar,a.[a / sofar];sofar,b.[b\000C / sofar];[];rp;rq) in
                                                rm-zeros(n - 1;cs)
    fi 
add-polyn(n;p;q) ==
  fix((λadd-polyn,n,p,q. if (n =z 0)
                        then p + q
                        else if p = Ax then q
                             otherwise if q = Ax then p
                                       otherwise eval rp = rev(p) in
                                                 eval rq = rev(q) in
                                                 eval cs = list_accum2(sofar,a,b.eval c = add-polyn (n - 1) a b in
                                                                                 [c / sofar];sofar,a.[a / sofar];sofar,b\000C.[b / 
                                                                                                    sofar];[];rp;rq) in
                                                   rm-zeros(n - 1;cs)
                        fi )) 
  n 
  p 
  q
Definitions occuring in Statement : 
rm-zeros: rm-zeros(n;p)
, 
list_accum2: list_accum2(x,a,b.f[x; a; b];x,a.g[x; a];x,b.h[x; b];y;as;bs)
, 
reverse: rev(as)
, 
cons: [a / b]
, 
nil: []
, 
callbyvalue: callbyvalue, 
ifthenelse: if b then t else f fi 
, 
eq_int: (i =z j)
, 
isaxiom: if z = Ax then a otherwise b
, 
apply: f a
, 
fix: fix(F)
, 
lambda: λx.A[x]
, 
subtract: n - m
, 
add: n + m
, 
natural_number: $n
Definitions occuring in definition : 
fix: fix(F)
, 
lambda: λx.A[x]
, 
ifthenelse: if b then t else f fi 
, 
eq_int: (i =z j)
, 
add: n + m
, 
isaxiom: if z = Ax then a otherwise b
, 
reverse: rev(as)
, 
list_accum2: list_accum2(x,a,b.f[x; a; b];x,a.g[x; a];x,b.h[x; b];y;as;bs)
, 
callbyvalue: callbyvalue, 
apply: f a
, 
cons: [a / b]
, 
nil: []
, 
rm-zeros: rm-zeros(n;p)
, 
subtract: n - m
, 
natural_number: $n
FDL editor aliases : 
add-polyn
Latex:
add-polyn(n;p;q)
==r  if  (n  =\msubz{}  0)
        then  p  +  q
        else  if  p  =  Ax  then  q
                  otherwise  if  q  =  Ax  then  p
                                      otherwise  eval  rp  =  rev(p)  in
                                                          eval  rq  =  rev(q)  in
                                                          eval  cs  =  list\_accum2(sofar,a,b.eval  c  =  add-polyn(n  -  1;a;b)  in
                                                                                                                          [c  /  sofar];sofar,a.[a  /  sofar];sofar,b\000C.[b  / 
                                                                                                                                                                sofar];[];rp;rq)  in
                                                              rm-zeros(n  -  1;cs)
        fi 
Latex:
add-polyn(n;p;q)  ==
    fix((\mlambda{}add-polyn,n,p,q.  if  (n  =\msubz{}  0)
                                                then  p  +  q
                                                else  if  p  =  Ax  then  q
                                                          otherwise  if  q  =  Ax  then  p
                                                                              otherwise  eval  rp  =  rev(p)  in
                                                                                                  eval  rq  =  rev(q)  in
                                                                                                  ...
                                                fi  )) 
    n 
    p 
    q
Date html generated:
2017_09_29-PM-05_59_51
Last ObjectModification:
2017_04_27-PM-04_41_40
Theory : integer!polynomials
Home
Index