Housekeeping derivations are T₂ derivations

theorem Undecidability.Thue.Matiyasevich1993.Compression.leftShape {n r : ℕ} (F E : Fin r → List (Fin n)) : Priority.LongShape (2 * t n r) (leftLong F E)

The transposed left long word begins with 2t copies of a and ends with b, exactly as required in the page-50 counting argument.

theorem Undecidability.Thue.Matiyasevich1993.Compression.rightShape {n r : ℕ} (F E : Fin r → List (Fin n)) : Priority.LongShape (2 * t n r) (rightLong F E)

The analogous shape theorem for the right long word.

def Undecidability.Thue.Matiyasevich1993.Compression.housekeepingIndex (i : Fin 4) : Fin 5

The inclusion of the four housekeeping-rule indices into the five priority-rule indices.

Equations

• Undecidability.Thue.Matiyasevich1993.Compression.housekeepingIndex i = Fin.castLE Undecidability.Thue.Matiyasevich1993.Compression.housekeepingIndex._proof_2 i

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Compression.stage₂F_housekeepingIndex (L : List Priority.A₂) (i : Fin 4) : stage₂F L (housekeepingIndex i) = Priority.housekeepingF i

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Compression.stage₂E_housekeepingIndex (M : List Priority.A₂) (i : Fin 4) : stage₂E M (housekeepingIndex i) = Priority.housekeepingE i

theorem Undecidability.Thue.Matiyasevich1993.Compression.firstStep_to_thueStep (L M : List Priority.A₂) {X Y : List Priority.A₂} (h : Priority.FirstStep X Y) : ThueStep (stage₂System L M) X Y

theorem Undecidability.Thue.Matiyasevich1993.Compression.firstEq_to_stage₂Eq (L M : List Priority.A₂) {X Y : List Priority.A₂} (h : Priority.FirstEq X Y) : ThueEq (stage₂System L M) X Y

Every directed first-priority reduction is also a derivation in the symmetric five-relation Thue system.

theorem Undecidability.Thue.Matiyasevich1993.Compression.simulate_binary {n r : ℕ} (F E : Fin r → List (Fin n)) {X Y : List (Fin 2)} (h : ThueEq (binarySystem F E) X Y) : ThueEq (stage₂System (leftLong F E) (rightLong F E)) (Priority.encode (u n r) X) (Priority.encode (u n r) Y)

Forward half of Matiyasevich's priority-compression equivalence: every binary rewrite, in arbitrary two-sided context, is simulated by the five-relation system on {a,b,e}.