Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Imperative programming (resit) / 3 / d / Solution

Let $S$ be the original sequence and $n=b-a$. The loop invariant isHere $\mathrm{bag}$ denotes the multiset of entries. The capacity condition uses the question's assumption of sufficient space. Removing two runs of combined length $z$ and appending their merge preserves the length and multiset. It also leaves all live values in one contiguous segment.

For a nonempty live sequence, let $R$ be its number of maximal initial runs obtained by repeatedly cutting at strict adjacent descents. The loop variant is $R-1$. If x = d, there is one run and the procedure returns a sorted permutation. Otherwise the iteration removes two runs and appends one; it cannot create a new descent inside that appended run. The appended run may join the last old run, further reducing $R$, so $R$ decreases by at least one. There are at most $R_0-1\le n-1$ merges.For $n=0$, the loop is skipped and the empty segment is already sorted. No global stability claim is needed: moving a merged run behind other runs can change the order of equal-labelled occurrences.