Strong convergence in posets

We consider the following solitaire game whose rules are reminiscent of the childrenʼs game of leapfrog. The game is played on a poset ( P , ≺ ) with n elements. The player is handed an arbitrary permutation π = ( x 1 , x 2 , … , x n ) of the elements in P. At each round an element may “skip over” a smaller element preceding it, i.e. swap positions with it. For example, if x i ≺ x i + 1 , then it is allowed to move from π to the permutation ( x 1 , x 2 , … , x i − 1 , x i + 1 , x i , x i + 2 , … , x n ) of Pʼs elements. The player is to carry out such steps as long as such swaps are possible. When there are several consecutive pairs of elements that satisfy this condition, the player can choose which pair to swap next. Does the playerʼs choice of swaps matter for the final permutation or is it uniquely determined by the initial order of Pʼs elements? The reader may guess correctly that the latter proposition is correct. What may be more surprising, perhaps, is that this question is not trivial. The proof works by constructing an appropriate system of invariants.