The power-of-two padding, transposition, and first priority block from Sections 2.3--2.4 of Matiyasevich (1995). This file is deliberately parameterized by the binary rule words; the preceding binary encoding stage supplies those words and their common-length/code-language properties.

@[reducible, inline]

abbrev Undecidability.Thue.Matiyasevich1993.Priority.A₂ : Type

The three-letter alphabet used in the priority stage.

Equations

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

def Undecidability.Thue.Matiyasevich1993.Priority.a : A₂

The first letter of the priority-stage alphabet.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.a = 0

def Undecidability.Thue.Matiyasevich1993.Priority.b : A₂

The second letter of the priority-stage alphabet.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.b = 1

def Undecidability.Thue.Matiyasevich1993.Priority.e : A₂

The separator letter of the priority-stage alphabet.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.e = 2

def Undecidability.Thue.Matiyasevich1993.Priority.exponent (r : ℕ) : ℕ

The exponent u for the least power t = 2^u not below r.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.exponent r = Nat.clog 2 r

def Undecidability.Thue.Matiyasevich1993.Priority.powerCount (r : ℕ) : ℕ

The number t of rows used in the transposed long relation.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.powerCount r = 2 ^ Undecidability.Thue.Matiyasevich1993.Priority.exponent r

theorem Undecidability.Thue.Matiyasevich1993.Priority.relationCount_le_powerCount (r : ℕ) : r ≤ powerCount r

theorem Undecidability.Thue.Matiyasevich1993.Priority.powerCount_pos (r : ℕ) : 0 < powerCount r

def Undecidability.Thue.Matiyasevich1993.Priority.paddedIndex {r : ℕ} (hr : 0 < r) (i : Fin (powerCount r)) : Fin r

Repeat the first relation when the original list is extended to 2^u relations. The paper repeats the last relation; either choice has the same effect.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.paddedIndex hr i = if h : ↑i < r then ⟨↑i, h⟩ else ⟨0, hr⟩

def Undecidability.Thue.Matiyasevich1993.Priority.paddedSide {r : ℕ} (hr : 0 < r) {α : Type u_1} (W : Fin r → List α) (i : Fin (powerCount r)) : List α

A rule-word family repeated to the least power-of-two row count.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.paddedSide hr W i = W (Undecidability.Thue.Matiyasevich1993.Priority.paddedIndex hr i)

def Undecidability.Thue.Matiyasevich1993.Priority.column {t : ℕ} (rows : Fin t → List (Fin 2)) (j : ℕ) : List (Fin 2)

A column of a rectangular family of words.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.column rows j = List.ofFn fun (i : Fin t) => (rows i).getD j 0

def Undecidability.Thue.Matiyasevich1993.Priority.columnsFrom {t : ℕ} (rows : Fin t → List (Fin 2)) : ℕ → ℕ → List (Fin 2)

Consecutive columns, starting at column j.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Thue.Matiyasevich1993.Priority.columnsFrom rows x✝ 0 = []

def Undecidability.Thue.Matiyasevich1993.Priority.transpose {t : ℕ} (width : ℕ) (rows : Fin t → List (Fin 2)) : List (Fin 2)

The column-major words L and M displayed at the bottom of page 48.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.transpose width rows = Undecidability.Thue.Matiyasevich1993.Priority.columnsFrom rows 0 width

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.columnsFrom_succ {t : ℕ} (rows : Fin t → List (Fin 2)) (j k : ℕ) : columnsFrom rows j (k + 1) = column rows j ++ columnsFrom rows (j + 1) k

theorem Undecidability.Thue.Matiyasevich1993.Priority.column_length {t : ℕ} (rows : Fin t → List (Fin 2)) (j : ℕ) : (column rows j).length = t

theorem Undecidability.Thue.Matiyasevich1993.Priority.columnsFrom_length {t width : ℕ} (rows : Fin t → List (Fin 2)) (start : ℕ) : (columnsFrom rows start width).length = width * t

theorem Undecidability.Thue.Matiyasevich1993.Priority.transpose_length {t width : ℕ} (rows : Fin t → List (Fin 2)) : (transpose width rows).length = width * t

theorem Undecidability.Thue.Matiyasevich1993.Priority.column_zero_of_starts_aa {t : ℕ} (rows : Fin t → List (Fin 2)) (hrows : ∀ (i : Fin t), ∃ (tail : List (Fin 2)), rows i = 0 :: 0 :: tail) : column rows 0 = List.replicate t 0

theorem Undecidability.Thue.Matiyasevich1993.Priority.column_one_of_starts_aa {t : ℕ} (rows : Fin t → List (Fin 2)) (hrows : ∀ (i : Fin t), ∃ (tail : List (Fin 2)), rows i = 0 :: 0 :: tail) : column rows 1 = List.replicate t 0

theorem Undecidability.Thue.Matiyasevich1993.Priority.transpose_starts_two_columns {t width : ℕ} (rows : Fin t → List (Fin 2)) (hwidth : 2 ≤ width) (hrows : ∀ (i : Fin t), ∃ (tail : List (Fin 2)), rows i = 0 :: 0 :: tail) : ∃ (tail : List (Fin 2)), transpose width rows = List.replicate (2 * t) 0 ++ tail

The long word begins with 2t copies of a, the fact used on page 50.

The first priority block

def Undecidability.Thue.Matiyasevich1993.Priority.pushE : List A₂ → List A₂

Move one e rightwards through pairs of binary letters. On a binary word this retains every second letter and leaves the e at the end.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Thue.Matiyasevich1993.Priority.pushE x✝ = Undecidability.Thue.Matiyasevich1993.Priority.e :: x✝

def Undecidability.Thue.Matiyasevich1993.Priority.firstNormal : List A₂ → List A₂

Canonical normalization for rules (20)--(23), processing from right to left.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Thue.Matiyasevich1993.Priority.firstNormal [] = []

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_a_cons (W : List A₂) : firstNormal (a :: W) = a :: firstNormal W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_b_cons (W : List A₂) : firstNormal (b :: W) = b :: firstNormal W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_e_cons (W : List A₂) : firstNormal (e :: W) = pushE (firstNormal W)

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.pushE_aa (W : List A₂) : pushE (a :: a :: W) = a :: pushE W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.pushE_ab (W : List A₂) : pushE (a :: b :: W) = b :: pushE W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.pushE_ba (W : List A₂) : pushE (b :: a :: W) = a :: pushE W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.pushE_bb (W : List A₂) : pushE (b :: b :: W) = b :: pushE W

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_prefix_congr (l : List A₂) {X Y : List A₂} (h : firstNormal X = firstNormal Y) : firstNormal (l ++ X) = firstNormal (l ++ Y)

def Undecidability.Thue.Matiyasevich1993.Priority.housekeepingF : Fin 4 → List A₂

The four left sides (20)--(23), using the local names for a,b,e.

Equations

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

def Undecidability.Thue.Matiyasevich1993.Priority.housekeepingE : Fin 4 → List A₂

The four right sides (20)--(23).

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_housekeeping (l r : List A₂) (i : Fin 4) : firstNormal (l ++ housekeepingF i ++ r) = firstNormal (l ++ housekeepingE i ++ r)

One use of a housekeeping rule in any two-sided context preserves the first priority normal form.

def Undecidability.Thue.Matiyasevich1993.Priority.FirstStep (X Y : List A₂) : Prop

One directed rewrite from the first priority block.

Equations

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

@[reducible, inline]

abbrev Undecidability.Thue.Matiyasevich1993.Priority.FirstEq (a : List A₂) : List A₂ → Prop

The reflexive transitive closure of the first-stage housekeeping rewrite relation.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.FirstEq = Relation.ReflTransGen Undecidability.Thue.Matiyasevich1993.Priority.FirstStep

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstStep_prefix (l : List A₂) {X Y : List A₂} (h : FirstStep X Y) : FirstStep (l ++ X) (l ++ Y)

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstEq_prefix (l : List A₂) {X Y : List A₂} (h : FirstEq X Y) : FirstEq (l ++ X) (l ++ Y)

theorem Undecidability.Thue.Matiyasevich1993.Priority.pushE_reachable (W : List A₂) : FirstEq (e :: W) (pushE W)

Greedily moving one e is itself a directed derivation.

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_reachable (W : List A₂) : FirstEq W (firstNormal W)

Every word reduces to the canonical value computed by firstNormal.

The e-count and the final alignment argument

def Undecidability.Thue.Matiyasevich1993.Priority.eCount (W : List A₂) : ℕ

The number of separator letters in a priority-stage word.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.eCount W = List.count Undecidability.Thue.Matiyasevich1993.Priority.e W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.eCount_nil : eCount [] = 0

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.eCount_append (X Y : List A₂) : eCount (X ++ Y) = eCount X + eCount Y

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.eCount_replicate_a (n : ℕ) : eCount (List.replicate n a) = 0

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.eCount_ae : eCount [a, e] = 1

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstStep_eCount {X Y : List A₂} (h : FirstStep X Y) : eCount X = eCount Y

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstEq_eCount {X Y : List A₂} (h : FirstEq X Y) : eCount X = eCount Y

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_eCount (W : List A₂) : eCount (firstNormal W) = eCount W

def Undecidability.Thue.Matiyasevich1993.Priority.liftBit (x : Fin 2) : A₂

Include a binary word into the alphabet {a,b,e}.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.liftBit x = Fin.castLE Undecidability.Thue.Matiyasevich1993.Priority.liftBit._proof_2 x

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

The inclusion of a binary word into the three-letter priority alphabet.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.liftBinary W = List.map Undecidability.Thue.Matiyasevich1993.Priority.liftBit W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.liftBinary_cons (x : Fin 2) (W : List (Fin 2)) : liftBinary (x :: W) = liftBit x :: liftBinary W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.liftBinary_append (X Y : List (Fin 2)) : liftBinary (X ++ Y) = liftBinary X ++ liftBinary Y

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.eCount_liftBinary (W : List (Fin 2)) : eCount (liftBinary W) = 0

theorem Undecidability.Thue.Matiyasevich1993.Priority.liftBit_injective : Function.Injective liftBit

theorem Undecidability.Thue.Matiyasevich1993.Priority.liftBinary_injective : Function.Injective liftBinary

def Undecidability.Thue.Matiyasevich1993.Priority.encode (u : ℕ) (W : List (Fin 2)) : List A₂

Equation (11) for i=1: append a e^u to the binary encoding.

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.Priority.encode_computable (u : ℕ) : Computable (encode u)

theorem Undecidability.Thue.Matiyasevich1993.Priority.encode_ne_nil (u : ℕ) (W : List (Fin 2)) : encode u W ≠ []

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.encode_eCount (u : ℕ) (W : List (Fin 2)) : eCount (encode u W) = u

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.pushE_replicate_e (u : ℕ) : pushE (List.replicate u e) = e :: List.replicate u e

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_replicate_e (u : ℕ) : firstNormal (List.replicate u e) = List.replicate u e

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_liftBinary_append (W : List (Fin 2)) (T : List A₂) : firstNormal (liftBinary W ++ T) = liftBinary W ++ firstNormal T

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_encode (u : ℕ) (W : List (Fin 2)) : firstNormal (encode u W) = encode u W

theorem Undecidability.Thue.Matiyasevich1993.Priority.stage₂_side_eCount (L M : List A₂) (hLM : eCount L = eCount M) (i : Fin 5) : eCount (stage₂F L i) = eCount (stage₂E M i)

theorem Undecidability.Thue.Matiyasevich1993.Priority.stage₂Step_eCount (L M : List A₂) (hLM : eCount L = eCount M) {X Y : List A₂} (h : ThueStep (stage₂System L M) X Y) : eCount X = eCount Y

theorem Undecidability.Thue.Matiyasevich1993.Priority.stage₂Eq_eCount (L M : List A₂) (hLM : eCount L = eCount M) {X Y : List A₂} (h : ThueEq (stage₂System L M) X Y) : eCount X = eCount Y

def Undecidability.Thue.Matiyasevich1993.Priority.NoAAA (W : List A₂) : Prop

Absence of a run aaa.

Equations

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

def Undecidability.Thue.Matiyasevich1993.Priority.HasARun (k : ℕ) (W : List A₂) : Prop

A word contains k consecutive copies of a.

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.Priority.hasARun_prefix (p : List A₂) {k : ℕ} {W : List A₂} (h : HasARun k W) : HasARun k (p ++ W)

theorem Undecidability.Thue.Matiyasevich1993.Priority.hasARun_of_le {m n : ℕ} {W : List A₂} (hmn : m ≤ n) (h : HasARun n W) : HasARun m W

theorem Undecidability.Thue.Matiyasevich1993.Priority.pushE_replicate_even (k : ℕ) (W : List A₂) : pushE (List.replicate (2 * k) a ++ W) = List.replicate k a ++ pushE W

On a binary run, pushE keeps every second letter.

theorem Undecidability.Thue.Matiyasevich1993.Priority.pushE_singleton_hasARun (x : A₂) (k : ℕ) (W : List A₂) : HasARun k (pushE (x :: List.replicate (2 * k) a ++ W))

A possible one-letter parity offset before an even run does not affect the sharp halving estimate.

theorem Undecidability.Thue.Matiyasevich1993.Priority.pushE_hasARun_half {k : ℕ} {W : List A₂} (h : HasARun (2 * k) W) : HasARun k (pushE W)

The sharp run estimate for one first-priority normalization step: one e can at most halve the length of an a-run.

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_replicate_a_append (n : ℕ) (W : List A₂) : firstNormal (List.replicate n a ++ W) = List.replicate n a ++ firstNormal W

theorem Undecidability.Thue.Matiyasevich1993.Priority.firstNormal_hasARun_scaled (X Y : List A₂) (k : ℕ) : HasARun k (firstNormal (X ++ List.replicate (2 ^ eCount X * k) a ++ Y))

After normalizing a prefix X, every one of its e letters can have halved a following run at most once.

theorem Undecidability.Thue.Matiyasevich1993.Priority.noAAA_not_hasARun_three {W : List A₂} (h : NoAAA W) : ¬HasARun 3 W

def Undecidability.Thue.Matiyasevich1993.Priority.LongRunRequirement (u run : ℕ) : Prop

The elementary but nontrivial run estimate invoked on page 50: destroying a run of run many a's while producing a first-block normal form with no aaa requires at least u occurrences of e in the left context.

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.Priority.longRunRequirement_two_power (u : ℕ) : LongRunRequirement u (2 * 2 ^ u)

The quantitative assertion used on page 50. The transposed long side starts with 2t = 2 * 2^u copies of a; if fewer than u priority letters occur to its left, at least four consecutive a's survive normalization.

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

The invariant furnished by equation (25): every reachable first priority normal form remains in the binary code language and hence has no aaa.

Equations

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

def Undecidability.Thue.Matiyasevich1993.Priority.LongShape (run : ℕ) (W : List A₂) : Prop

The exact shape needed from the transposed words: the initial 2t copies of a and a final b.

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.Priority.phi₂_residual_long_context {run : ℕ} {W : List A₂} (hshape : LongShape run W) (l : List (Fin 2)) (R : List A₂) : ∃ (middle : List Matiyasevich1993.A₂), phi₂ (l ++ rho₂ W ++ 0 :: rho₂ R) = phi₂ l ++ List.replicate run a ++ middle ++ [a, e] ++ R

Decode a long side with a residual d inside arbitrary contexts.

Excluding the residual decoder alignment

theorem Undecidability.Thue.Matiyasevich1993.Priority.long_aligned_of_decoded_reachable {u run : ℕ} {L M X : List A₂} {W : List (Fin 2)} (hLM : eCount L = eCount M) (hX : eCount X = u) (hNoAAA : ReachableNoAAA L M X) (hRun : LongRunRequirement u run) (hshapeL : LongShape run L) (hshapeM : LongShape run M) (hdecode : ThueEq (stage₂System L M) X (phi₂ W)) (l r : List (Fin 2)) : W = l ++ rho₂ L ++ r ∨ W = l ++ rho₂ M ++ r → rho₂ (phi₂ r) = r

If the two invariants isolated on page 50 hold, then an occurrence of the long final relation cannot be followed by the residual unmatched d. This is the counting core of the converse T₃ → T₂: the initial run of a's forces all u priority letters into the left context, while decoding the residual d creates one additional e.

theorem Undecidability.Thue.Matiyasevich1993.Priority.final_decode_and_aligned {u run : ℕ} {L M X : List A₂} {W : List (Fin 2)} (hLM : eCount L = eCount M) (hX : eCount X = u) (hNoAAA : ReachableNoAAA L M X) (hRun : LongRunRequirement u run) (hshapeL : LongShape run L) (hshapeM : LongShape run M) (hfinal : ThueEq (baseSystem (rho₂ L) (rho₂ M)) (rho₂ X) W) : ThueEq (stage₂System L M) X (phi₂ W) ∧ ∀ (l r : List (Fin 2)), W = l ++ rho₂ L ++ r ∨ W = l ++ rho₂ M ++ r → rho₂ (phi₂ r) = r

Simultaneously decode a final-system derivation and establish the alignment invariant required for its next long-rule step. The simultaneous induction avoids any circularity: alignment at the current word decodes the next step, and the decoded prefix derivation re-establishes alignment at the new word by long_aligned_of_decoded_reachable.

theorem Undecidability.Thue.Matiyasevich1993.Priority.longRuleAlignedFrom_of_invariants {u run : ℕ} {L M X : List A₂} (hLM : eCount L = eCount M) (hX : eCount X = u) (hNoAAA : ReachableNoAAA L M X) (hRun : LongRunRequirement u run) (hshapeL : LongShape run L) (hshapeM : LongShape run M) : LongRuleAlignedFrom L M X

The page-50 invariants imply the exact alignment predicate consumed by the final-stage reflection theorem.

theorem Undecidability.Thue.Matiyasevich1993.Priority.rho₂_iff_of_priority_invariants {u run : ℕ} {L M X : List A₂} (hLM : eCount L = eCount M) (hX : eCount X = u) (hNoAAA : ReachableNoAAA L M X) (hRun : LongRunRequirement u run) (hshapeL : LongShape run L) (hshapeM : LongShape run M) (Y : List A₂) : ThueEq (stage₂System L M) X Y ↔ ThueEq (baseSystem (rho₂ L) (rho₂ M)) (rho₂ X) (rho₂ Y)

A convenient conditional form of equivalence (10), with the two priority invariants made explicit.