Data Structures, Algorithms, & Applications in C++
Chapter 9, Exercise 21

The restrictions on car moves are
1.
A car may be moved from the front (i.e., right end) of the input track to the rear of one of the holding tracks or to the left end of the output track.
2.
A car may be moved from the front of a holding track to the left end of the output track.

With these restrictions Program 9.6 does indeed succeed in rearranging cars whenever a k track rearrangement is possible.

To prove this suppose that there is a rearrangeable k track input permutation on which Program 9.6 fails. Let S = s1, s2, s3, ..., be a sequence of car moves that uses at most k tracks and succeeds in rearranging the cars. Consider the car moves F = f1, f2, f3, ..., fq made by Program 9.6 up to the point it declared failure. Our proof strategy is to successively transform S into the sequences S1, S2, S3, ..., Sp such that each sequence is a valid way to rearrange the cars using at most k tracks and the front part of Sp is the same as F. Now, since the move sq+1 is valid for Sp, it must be valid for F because the track configurations are identical at this time in both Sp and F. So, Program 9.6 could not fail with the sequence F, contradicting the assumption that the program did fail.

To obtain Sp as above, find the smallest i, i <= q such that si is different from fi. If such an i does not exist S is the sequence Sp and we are done. So assume that i exists.

si cannot be a move that moves a car to the output track as Program 9.6 moves cars to the output track as soon as it is possible to do so and si and fi are different. If fi moves car u to the output track, then we may alter the move sequence S to do the same now and delete from S its later move that moves car u to the output track. This change in S does not affect the correctness of the move sequence and yields the rearrangement sequence S1.

If neither si nor fi moves a car to the output track, both move the next input car to a holding track; but the holding track a the car is moved to by S is different from the holding track b it is moved to by F. Change si to move the car to the holding track b instead and change all future moves of S that move a car to track a to move the car to track b and vice versa. The new sequence is S1. Notice that these changes preserve the property that cars on a track are in increasing order from front to rear and so the sequence S1 remains a valid rearrangement sequence.

By performing the above transformations first on S to get S1, then on S1, to get S2, and so on, we eventually obtain Sp and we are done.