Finite Rearrangment

Theorem 1. Given preferential commutation:

B_{i+1 .. n}B_{i} ⊆ B_{0}B_{0 .. n}^{∗} ∪ B_{i}^{+} ∪ B_{i+1 .. n} for all i = 0 .. n − 1

and given that each B_{i} is well-founded. we have that any chain in the union of the B_{i} can be replaced by a sequence of B_{i} steps with nondecreasing indices:

B_{0 .. n}^{∗} ⊆ B_{0}^{∗}B_{1}^{∗} ⋯ B_{n}^{∗}.

Compare [?, Thm. 54].

Proof. Suppose there is a chain s B_{0 .. n}^{∗} t from s to t. We look for inversions and replace them.

Analogous to our previous use of constricting steps B_{i}^{−}, let C_{i} be B_{i} (i ≥ 1) with the constraint that there is no chain leading out of the source u of a step u B_{i} w that begins with an A = B_{0} step u A v, continues with arbitrary B = B_{0 .. n} steps and ends up at t. That is,

u C_{i} w B^{∗} t

if

u B_{i} w B^{∗} t

but there is no

u A v B^{∗} t

Since A is well-founded, we can construct a B path that takes the preferred A whenever it is possible to do so and still arrive eventually at t. That leaves us with a chain s (A ∪ C)^{∗} t, where C is short for C_{1 .. n}. Any B-step taken is a constricted C-step.

We are given (for i = 0) that

B_{1 .. n}A ⊆ AB^{∗} ∪ A^{+} ∪ B_{1 .. n}

which means that

CA ⊆ C

since, in this case, an initial A-step is precluded. This implies that all the non-initial A-steps in s (A ∪ C)^{∗} t can be erased, leaving s A^{∗}C^{∗} t.

Consider again the preferential condition,

B_{i+1 .. n}B_{i} ⊆ AB_{0 .. n}^{∗} ∪ B_{i}^{+} ∪ B_{i+1 .. n}

This implies

C_{i+1 .. n}B_{i} ⊆ C_{i}B_{i}^{∗} ∪ C_{i+1 .. n}

By an easy induction

C_{i+1 .. n}B_{i}^{∗} ⊆ C_{i}B_{i}^{∗} ∪ C_{i+1 .. n}

By another induction

(C_{i+1 .. n}B_{i}^{∗})^{∗} ⊆ B_{i}^{∗}C_{i+1 .. n}^{∗}

This is because

(C_{i+1 .. n}B_{i}^{∗})(C_{i+1 .. n}B_{i}^{∗})^{∗} ⊆ (C_{i}B_{i}^{∗} ∪ C_{i+1 .. n})B_{i}^{∗}C_{i+1 .. n}^{∗}
⊆ C_{i}B_{i}^{∗}C_{i+1 .. n}^{∗} ∪ (C_{i+1 .. n}B_{i}^{∗})C_{i+1 .. n}^{∗}
⊆ B_{i}^{∗}C_{i+1 .. n}^{∗}

Applying

(C_{i+1 .. n}B_{i}^{∗})^{∗} ⊆ B_{i}^{∗}C_{i+1 .. n}^{∗}

repeatedly, for i = 1, …, n − 1, moves lower-indexed relations to the left and results in

s A^{∗}B_{1}^{∗}B_{2}^{∗} ⋯ B_{n}^{∗} t

as claimed. ⊓ ⊔

How much wellfoundedness is actually needed?