Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 2 / a / 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 givesFor 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:HenceOnly 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.