Nuprl Definition : add-polynom

add-polynom(p;q)
==r if tree_leaf?(p)
      then if tree_leaf?(q)
           then eval a = tree_leaf-value(p) + tree_leaf-value(q) in
                tree_leaf(a)
           else eval a = add-polynom(p;tree_node-left(q)) in
                eval b = tree_node-right(q) in
                  tree_node(a;b)
           fi 
    if tree_leaf?(q) then eval a = add-polynom(tree_node-left(p);q) in eval b = tree_node-right(p) in   tree_node(a;b)
    else eval a = add-polynom(tree_node-left(p);tree_node-left(q)) in
         eval b = add-polynom(tree_node-right(p);tree_node-right(q)) in
           if poly-zero(b) ∧b poly-int(a) then a else tree_node(a;b) fi 
    fi 
add-polynom(p;q) ==
  fix((λadd-polynom,p,q. if tree_leaf?(p)
                           then if tree_leaf?(q)
                                then eval a = tree_leaf-value(p) + tree_leaf-value(q) in
                                     tree_leaf(a)
                                else eval a = add-polynom p tree_node-left(q) in
                                     eval b = tree_node-right(q) in
                                       tree_node(a;b)
                                fi 
                        if tree_leaf?(q)
                          then eval a = add-polynom tree_node-left(p) q in
                               eval b = tree_node-right(p) in
                                 tree_node(a;b)
                        else eval a = add-polynom tree_node-left(p) tree_node-left(q) in
                             eval b = add-polynom tree_node-right(p) tree_node-right(q) in
                               if poly-zero(b) ∧b poly-int(a) then a else tree_node(a;b) fi 
                        fi )) 
  p 
  q


Wellformedness Lemmas :  add-polynom_wf,  add-polynom_wf1
Definitions occuring in Statement :  poly-int: poly-int(p),  poly-zero: poly-zero(p),  tree_node-right: tree_node-right(v),  tree_node-left: tree_node-left(v),  tree_leaf-value: tree_leaf-value(v),  tree_leaf?: tree_leaf?(v),  tree_node: tree_node(left;right),  tree_leaf: tree_leaf(value),  band: p ∧b q,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  add: n + m
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  add: n + m,  tree_leaf-value: tree_leaf-value(v),  tree_leaf: tree_leaf(value),  tree_leaf?: tree_leaf?(v),  tree_node-left: tree_node-left(v),  callbyvalue: callbyvalue,  apply: f a,  tree_node-right: tree_node-right(v),  ifthenelse: if b then t else f fi ,  band: p ∧b q,  poly-zero: poly-zero(p),  poly-int: poly-int(p),  tree_node: tree_node(left;right)
FDL editor aliases :  add-polynom
Latex:
add-polynom(p;q)
==r  if  tree\_leaf?(p)
            then  if  tree\_leaf?(q)
                      then  eval  a  =  tree\_leaf-value(p)  +  tree\_leaf-value(q)  in
                                tree\_leaf(a)
                      else  eval  a  =  add-polynom(p;tree\_node-left(q))  in
                                eval  b  =  tree\_node-right(q)  in
                                    tree\_node(a;b)
                      fi 
        if  tree\_leaf?(q)
            then  eval  a  =  add-polynom(tree\_node-left(p);q)  in
                      eval  b  =  tree\_node-right(p)  in
                          tree\_node(a;b)
        else  eval  a  =  add-polynom(tree\_node-left(p);tree\_node-left(q))  in
                  eval  b  =  add-polynom(tree\_node-right(p);tree\_node-right(q))  in
                      if  poly-zero(b)  \mwedge{}\msubb{}  poly-int(a)  then  a  else  tree\_node(a;b)  fi 
        fi 

Latex:
add-polynom(p;q)  ==
    fix((\mlambda{}add-polynom,p,q.  if  tree\_leaf?(p)
                                                      then  if  tree\_leaf?(q)
                                                                then  eval  a  =  tree\_leaf-value(p)  +  tree\_leaf-value(q)  in
                                                                          tree\_leaf(a)
                                                                else  eval  a  =  add-polynom  p  tree\_node-left(q)  in
                                                                          eval  b  =  tree\_node-right(q)  in
                                                                              tree\_node(a;b)
                                                                fi 
                                                if  tree\_leaf?(q)
                                                    then  eval  a  =  add-polynom  tree\_node-left(p)  q  in
                                                              eval  b  =  tree\_node-right(p)  in
                                                                  tree\_node(a;b)
                                                else  eval  a  =  add-polynom  tree\_node-left(p)  tree\_node-left(q)  in
                                                          eval  b  =  add-polynom  tree\_node-right(p)  tree\_node-right(q)  in
                                                              if  poly-zero(b)  \mwedge{}\msubb{}  poly-int(a)  then  a  else  tree\_node(a;b)  fi 
                                                fi  )) 
    p 
    q


Date html generated: 2017_10_01-AM-08_32_42
Last ObjectModification: 2017_05_02-PM-06_00_21

Theory : integer!polynomial!trees


Home Index