We'll show that the algorithm has the following property:

It transforms a sequence of the form

(any elements) | (ascending sequence)

into

(any elements) | (reversed sequence)

going through all the permutations of the tail sequence

For example, if the algorithm is launched on the sequence

2 | 1 3 4

then it transforms it in 5 steps to the sequence

2 | 4 3 1

Let us prove this by induction. It is clear that the algorithm does just that when the length of the ascending tail sequence is 2.

Now suppose we have a ascending tail sequence, like this:

a₀ ... a_k ... a_n-1

where a_k < a_k+1 < ... < a_n-1.

By induction, the algorithm first permutes the shorter tail sequence a_k+1 ... a_n-1 until it is completely reversed to

a₀ ... a_k a_n-1 ... a_k+1.

Now the algorithm picks the smallest element larger than a_k and swaps it (which keeps the tail sequence descending) and then reverses the tail which makes it ascending. Again, by the inductive assumption, the shorter tail sequence is now being subjected to all of its permutations until it is reversed.

To complete the argument, observe that after each reversal of the shorter tail a larger element is extracted from the shorter tail. Ultimately, the largest element is extracted and the shorter tail is reversed one last time, leading to the reversal of the longer tail.