Section 2.5: T₂ to the final binary three-rule system

@[reducible, inline]

abbrev Undecidability.Thue.Matiyasevich1993.A₂ : Type

The letters a, b, and e of the penultimate alphabet.

Equations

• Undecidability.Thue.Matiyasevich1993.A₂ = Fin 3

@[reducible, inline]

abbrev Undecidability.Thue.Matiyasevich1993.finalLetterA : A₂

The first letter of the three-letter alphabet used in the final binary encoding.

Equations

• Undecidability.Thue.Matiyasevich1993.finalLetterA = 0

@[reducible, inline]

abbrev Undecidability.Thue.Matiyasevich1993.finalLetterB : A₂

The second letter of the three-letter alphabet used in the final binary encoding.

Equations

• Undecidability.Thue.Matiyasevich1993.finalLetterB = 1

@[reducible, inline]

abbrev Undecidability.Thue.Matiyasevich1993.finalLetterE : A₂

The third letter of the three-letter alphabet used in the final binary encoding.

Equations

• Undecidability.Thue.Matiyasevich1993.finalLetterE = 2

def Undecidability.Thue.Matiyasevich1993.rho₂Letter : A₂ → List (Fin 2)

Equation (26), with c = 1 and d = 0.

Equations

• Undecidability.Thue.Matiyasevich1993.rho₂Letter = ![[1], [1, 0], [0, 0]]

def Undecidability.Thue.Matiyasevich1993.rho₂ (W : List A₂) : List (Fin 2)

The homomorphic extension of ρ₂ to words.

Equations

• Undecidability.Thue.Matiyasevich1993.rho₂ W = List.flatMap Undecidability.Thue.Matiyasevich1993.rho₂Letter W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.rho₂_cons (x : A₂) (W : List A₂) : rho₂ (x :: W) = rho₂Letter x ++ rho₂ W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.rho₂_append (X Y : List A₂) : rho₂ (X ++ Y) = rho₂ X ++ rho₂ Y

theorem Undecidability.Thue.Matiyasevich1993.rho₂_computable : Computable rho₂

def Undecidability.Thue.Matiyasevich1993.phi₂Aux : List (Fin 2) → List A₂

The right-to-left decoder φ₂ from page 51, expressed on the reversed input. Reversed codewords are 1, 01, and 00; a lone leading 0 is the single possible unmatched d.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Thue.Matiyasevich1993.phi₂Aux [] = []
• Undecidability.Thue.Matiyasevich1993.phi₂Aux [y] = if y = 1 then Undecidability.Thue.Matiyasevich1993.finalLetterA :: Undecidability.Thue.Matiyasevich1993.phi₂Aux [] else []

def Undecidability.Thue.Matiyasevich1993.phi₂ (W : List (Fin 2)) : List A₂

The inverse map φ₂ in the orientation used in the paper.

Equations

• Undecidability.Thue.Matiyasevich1993.phi₂ W = (Undecidability.Thue.Matiyasevich1993.phi₂Aux W.reverse).reverse

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.phi₂_rho₂ (W : List A₂) : phi₂ (rho₂ W) = W

φ₂ is a left inverse to the binary encoding, as required below (26).

theorem Undecidability.Thue.Matiyasevich1993.phi₂_append_rho₂ (X : List (Fin 2)) (W : List A₂) : phi₂ (X ++ rho₂ W) = phi₂ X ++ W

Appending a complete encoded word cannot interact with the decoding of the prefix. This is the algebraic form of the right-to-left parsing used on page 52.

theorem Undecidability.Thue.Matiyasevich1993.phi₂_context_rho₂ (l : List (Fin 2)) (X Y : List A₂) : phi₂ (l ++ rho₂ X ++ rho₂ Y) = phi₂ l ++ X ++ Y

def Undecidability.Thue.Matiyasevich1993.rho₂Reverse (W : List A₂) : List (Fin 2)

The word encoding obtained by reversing the input and output of ρ₂.

Equations

• Undecidability.Thue.Matiyasevich1993.rho₂Reverse W = (Undecidability.Thue.Matiyasevich1993.rho₂ W.reverse).reverse

theorem Undecidability.Thue.Matiyasevich1993.rho₂_phi₂_reconstruct (W : List (Fin 2)) : rho₂ (phi₂ W) = W ∨ 0 :: rho₂ (phi₂ W) = W

Equivalently, every binary word is either exactly an encoded word or is an encoded word preceded by the unmatched letter d.

The converse to rho₂_forward is deliberately not stated for arbitrary T₂ words. Equivalence (10) only applies to words obtained from the original T₀ words by the preceding encodings. Matiyasevich's converse on pages 50--52 uses two invariants of those reachable words:

1. the priority normal form has no run of more than two a's;
2. it has exactly u occurrences of e, all forced to lie to the left of an occurrence of the long rule.

These invariants rule out the sole bad decoder alignment: the unmatched d from rho₂_phi₂_reconstruct immediately following ρ₂(L) or ρ₂(M). Treating rho₂ as an unrestricted embedding would therefore assert a stronger statement than the paper proves.

def Undecidability.Thue.Matiyasevich1993.stage₂F (L : List A₂) : Fin 5 → List A₂

The five left sides (20)--(24) of T₂.

Equations

• One or more equations did not get rendered due to their size.

def Undecidability.Thue.Matiyasevich1993.stage₂E (M : List A₂) : Fin 5 → List A₂

The five right sides (20)--(24) of T₂.

Equations

• One or more equations did not get rendered due to their size.

def Undecidability.Thue.Matiyasevich1993.stage₂System (L M : List A₂) : ThueSystem A₂

The five-rule priority-stage Thue system parametrized by its long relation.

Equations

• One or more equations did not get rendered due to their size.

theorem Undecidability.Thue.Matiyasevich1993.rho₂_rule (L M : List A₂) (i : Fin 5) : ThueEq (baseSystem (rho₂ L) (rho₂ M)) (rho₂ (stage₂F L i)) (rho₂ (stage₂E M i))

Each of the five rules of T₂ is simulated by the final three rules. The middle two housekeeping simulations use the first or second final rule in a one-letter right context.

theorem Undecidability.Thue.Matiyasevich1993.rho₂_step (L M : List A₂) {X Y : List A₂} (h : ThueStep (stage₂System L M) X Y) : ThueEq (baseSystem (rho₂ L) (rho₂ M)) (rho₂ X) (rho₂ Y)

Forward half of equivalence (10) for the last stage.

theorem Undecidability.Thue.Matiyasevich1993.rho₂_forward (L M : List A₂) {X Y : List A₂} (h : ThueEq (stage₂System L M) X Y) : ThueEq (baseSystem (rho₂ L) (rho₂ M)) (rho₂ X) (rho₂ Y)

Forward half of equivalence (10) for arbitrary derivations.

theorem Undecidability.Thue.Matiyasevich1993.rho₂_ne_nil {W : List A₂} (hW : W ≠ []) : rho₂ W ≠ []

Every nonempty T₂ word has nonempty binary encoding.

theorem Undecidability.Thue.Matiyasevich1993.phi₂_short_rule (L M : List A₂) (i : Fin 3) (hi : i ≠ 2) (l r : List (Fin 2)) : ThueEq (stage₂System L M) (phi₂ (l ++ baseF (rho₂ L) i ++ r)) (phi₂ (l ++ baseE (rho₂ M) i ++ r))

A use of either short final relation always decodes to one of the four housekeeping relations (20)--(23). Which one is selected is determined by the single residual d at the beginning of the right context.

theorem Undecidability.Thue.Matiyasevich1993.phi₂_long_rule_aligned (L M : List A₂) (l r : List (Fin 2)) (hr : rho₂ (phi₂ r) = r) : ThueEq (stage₂System L M) (phi₂ (l ++ baseF (rho₂ L) 2 ++ r)) (phi₂ (l ++ baseE (rho₂ M) 2 ++ r))

The long final relation also decodes directly when the right context is aligned. Thus the only unformalized case in the last-stage converse is the long relation together with the residual alternative 0 :: rho₂ (phi₂ r) = r.

def Undecidability.Thue.Matiyasevich1993.LongRuleAlignedFrom (L M X : List A₂) : Prop

The exact reachability invariant needed to rule out the bad long-rule alignment on pages 50--52.

Equations

• One or more equations did not get rendered due to their size.

theorem Undecidability.Thue.Matiyasevich1993.phi₂_step_of_long_aligned (L M : List A₂) {X Y : List (Fin 2)} (haligned : ∀ (l r : List (Fin 2)), X = l ++ rho₂ L ++ r ∨ X = l ++ rho₂ M ++ r → rho₂ (phi₂ r) = r) (h : ThueStep (baseSystem (rho₂ L) (rho₂ M)) X Y) : ThueEq (stage₂System L M) (phi₂ X) (phi₂ Y)

theorem Undecidability.Thue.Matiyasevich1993.rho₂_reflect_of_longRuleAligned (L M X Y : List A₂) (hsafe : LongRuleAlignedFrom L M X) (h : ThueEq (baseSystem (rho₂ L) (rho₂ M)) (rho₂ X) (rho₂ Y)) : ThueEq (stage₂System L M) X Y

Conditional converse for the final stage. The rewriting and decoder bookkeeping reduce precisely to LongRuleAlignedFrom, supplied by the e-count and priority-normal-form invariants of Section 2.4.

theorem Undecidability.Thue.Matiyasevich1993.rho₂_iff_of_longRuleAligned (L M X : List A₂) (hsafe : LongRuleAlignedFrom L M X) (Y : List A₂) : ThueEq (stage₂System L M) X Y ↔ ThueEq (baseSystem (rho₂ L) (rho₂ M)) (rho₂ X) (rho₂ Y)