Is there a proof of the recursive algorithm for generating all permutations of a sequence?

Question

For clarity, I attach below a concise implementation of the algorithm in Python. I understand that it checks all possible element swaps, but I don't see how that necessarily means that all possible orderings of the elements will be reached, and/or that no ordering will be duplicated.

For example, what if the elements at index 0 and 1 are swapped, then 1 and 2 are swapped? How does the algorithm guarantee this won't result in a duplicate ordering?

P = []
def permute(l, n=0):
    if n == len(l):
        return P.append(list(l))
    for i in xrange(n, len(l)):
        l[i], l[n] = l[n], l[i]
        permute(l, n+1)
        l[i], l[n] = l[n], l[i]

Answer 1

Hint: Prove by induction that $\mathrm{permute}(l,n)$:

• Adds to $P$ all permutations obtained from $l$ by permuting coordinates $n,\ldots,|l|$.
• Leaves $l$ unchanged. That is, the value of $l$ after running the function is the same as its value before running it.

Answer 2

Another option, just to show that you can think out of the box. You can prove that:

1. The algorithm appends exactly factorial(len(l)) permutations to P;
2. No permutation is appended twice.