Correctness proof of the algoritm to generate permutations in lexicographic order
One can try to come up with the algorithm by oneself (thereby proving its correctness) after incremental understanding of: (a) how to define a permutation as &quot;larger&quot; (lexciographically) than another one, (b) what really the very next permutation of $P$ &quot;looks like&quot; compared to $P$ (how/where it differs from $P$). Once we find-out some properties, we may be able to write this algorithm ourselves.
Some outline:

define the &quot;lexicographic order&quot; of permutations $P_1$ and $P_2$. Say, $k$ is the very first index at which they differ. Then the &quot;order&quot; of their elements at index $k$ decides the &quot;lexicographic order&quot; of $P_1$ and $P_2$.

So what should be the smallest and largest permutation of array $a$ ?

Suppose array $a$ currently holds permutation $P$. Say $P'$ is the very next permutation of $P$ in the lexicographic-order, and they first differ at index $k$. Now, use the definition in (1) and the observation in (2) to find out what is the structure of elements in $P/P'$ at index $k$ and after it. You can argue that:



elements in $P$ after $k$ must form a decreasing-sequence (call it $S$).
element in $P$ at $k$ must be smaller than the largest element of $S$, which is $a[k+1]$.
due to above, we must have an element $a[l]$ in $S$ which is the smallest element in $S$ larger than $a[k]$. In $P'$, this element must appear at index $k$.
so the remaining (after $k$) elements of $P'$ are simply $S$ with $a[l]$ removed and $a[k]$ added.
these remaining (after $k$) elements of $P'$, must be in increasing order (for $P'$ to be the smallest possible, but larger than $P$). The 4th step in the posted algorithm is simply obtaining this increasing order by reversing the existing decreasing-sequence $S$ (now modified via swap, but continues to remain decreasing).

(For further details, refer to section &quot;Lexicographical Order&quot; in this).