= Solution
Let $S$ be the original <sequence> and $n=b-a$. The <loop invariant> is
$$
0\leq c\leq d\leq N,\qquad d-c=n,\qquad
\operatorname{bag}(u[c..d))=\operatorname{bag}(S).
$$
Here $\operatorname{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\leq n-1$ merges.
$$
\boxed{\text{Preserved length and multiset, plus decreasing run count, imply total correctness}.}
$$
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.
Back to article page
