Solution (source code)

= Solution

There is an index slip in the source: starting with $G_1$ and performing steps $1,\ldots,n$ produces the final graph $G_{n+1}$. Write $H$ for that final graph. The literal assertion for $G_n$ can fail: take a triangle with $\ell(xz)=3$, $\ell(xy)=2$, $\ell(yz)=1$. Before the final step the extra edge $yz$ remains; only the final deletion removes it.

The invariant is that $x$ and $y$ remain connected. Choose a simple $xy$ <graph path> $P$ in $H$. If an edge of $H$ did not lie in $P$, then at its processing time $P$ was still present and avoided that edge. The algorithm would therefore have deleted it, a contradiction. Thus every edge of $H$ lies in $P$. \b[The final graph is precisely an $xy$ path and possibly isolated vertices.]