Complex property of sparse horner polynomials by induction
You need to use induction on some complexity measure $\mu(x,y)$ (on some well-ordered domain) which has the following property:


  When running the addition procedure on $x,y$, all recursive calls are on pairs $z,w$ for which $\mu(z,w) &lt; \mu(x,y)$.


A complexity measure satisfying this property shows that the addition procedure terminates, and will also allow you to do a proof by induction. Note that you are not splitting into cases according to the coarse structure of $x,y$.

It is often the case that you can take $\mu(x,y)$ to be the total description length of $x,y$, so you might start by checking whether this works here. Another possibility is to take the sum of the total degrees of all monomials in $x,y$.

Finally, how should you approach the problem? I suggest forgetting about the formalism (in particular, ignoring POP completely) and writing out the simplification steps in their barest forms. Using $N(p,q)$ for the normal form of $p+q$ (themselves already in normal form), the rules are:


$N(c_1,c_2) = c_1+c_2$.
$N(c,x_i^jp+q) = x_i^jp+N(c,q)$.
$N(x_i^{j_1}p_1+q_1,x_i^{j_2}p_2+q_2) = x_i^{j_2}N(x_i^{j_1-j_2}p_1+0,p_2)+N(q_1,q_2)$, where $j_1 &gt; j_2$.
$N(x_i^jp_1+q_1,x_i^jp_2+q_2) = x_i^jN(p_1,p_2)+N(q_1,q_2)$.
$N(x_{i_1}^{j_1}p_1+q_1,x_{i_2}^{j_2}p_2+q_2) = x_{i_1}^{j_1}p_1+N(q_1,x_{i_2}^{j_2}p_2+q_2)$, where $i_1 &lt; i_2$.


Here we are conflating POP and POW, which makes things a littler more concrete.

We want to prove that these rules are correct, namely:


  If $p,q$ are in normal form then $N(p,q)$ terminates, is in normal form, and agrees as a function with $p+q$.


This can be split into several tasks. First, assuming that $p,q$ are in normal form, show that they match exactly one rule. Second, show that in each recursive invocation $N(r,s)$ on the right-hand side, (i) $\mu(r,s) &lt; \mu(p,q)$, and (ii) $r,s$ are in normal form. Third, show that the right-hand side agrees with $p+q$ as a polynomials (using the inductive hypothesis). Fourth, show that the right-hand side is in normal form (again using the inductive hypothesis).

Proving that the addition procedure as given is valid is similar, only we need to take into account the different encoding which separates POW and POP.