Add a little explanation using the convolution property in a step for both
explanation of checks and swaps recurrences.

Fix an error in the swaps proof about the step before the final form of S(t).
Add an observation that [t^n]a(t) returns a function of n.