= Solution
Use <structural induction> on the finite <list> `xs`, strengthening the <induction hypothesis> to hold for every accumulator value $y$. For the empty <list>, the defining equation of the <left fold> gives
$$
x\oplus\operatorname{foldl}(\otimes)\,y\,[]
=x\oplus y
=\operatorname{foldl}(\otimes)\,(x\oplus y)\,[].
$$
For the inductive step, suppose the identity holds for the tail `zs` and every accumulator. Expand the first <left fold>, apply the <induction hypothesis> at accumulator $y\otimes z$, and then use the supplied compatibility law:
$$
\begin{aligned}
x\oplus\operatorname{foldl}(\otimes)\,y\,(z:\mathrm{zs})
&=x\oplus\operatorname{foldl}(\otimes)\,(y\otimes z)\,\mathrm{zs}\\
&=\operatorname{foldl}(\otimes)\,(x\oplus(y\otimes z))\,\mathrm{zs}\\
&=\operatorname{foldl}(\otimes)\,((x\oplus y)\otimes z)\,\mathrm{zs}\\
&=\operatorname{foldl}(\otimes)\,(x\oplus y)\,(z:\mathrm{zs}).
\end{aligned}
$$
Hence
$$
\boxed{x\oplus\operatorname{foldl}(\otimes)\,y\,\mathrm{xs}=\operatorname{foldl}(\otimes)\,(x\oplus y)\,\mathrm{xs}.}
$$
Only equation (1) is needed for this part; the seed condition in equation (2) enters the next proof. Quantifying over the accumulator is essential because the recursive call changes it.
Back to article page
