Associativity rotations connect all complete reductions

Exact statement

After adjoining the contextual overlap move $((AB)C)\leftrightarrow(A(BC))$ to the disjoint-square moves, every pair of complete occurrence-labelled reductions $a^n\Rightarrow^*a$ is connected.

StatusProved for complete reductions in the stated model

External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

Disjoint squares account only for changes in scheduling. Overlap moves change the underlying binary merge tree.

Definitions

The overlap move replaces the two complete length-two reductions represented by $((AB)C)$ and $(A(BC))$ , and is closed under surrounding derivation contexts.

Hypotheses and scope

Complete occurrence-labelled reductions in $R=\{aa\to a\}$ .

Proof or evidence

By CRD-RW-1a, disjoint squares connect all histories with the same merge tree. The overlap move induces an ordinary rotation of planar full binary trees. Repeated rotations take every such tree to the right comb, so the augmented transformation graph is connected.

Rotation connectedness proof →

Verification notes

The preserved proof was checked for the required contextual closure and for the distinction between complete length-two paths and isolated first steps.

Limitations

Connectedness does not imply simple connectedness or higher coherence.
The overlap relation requires precomposition, postcomposition, and derivation-context closure.

Open work

Determine which higher cells are required for coherence beyond connectedness.