The binary coding stage in Section 2.3 of Matiyasevich (1995). If the source alphabet has N letters, the (zero-based) form of (18) is

a_j ↦ a a b^(j+1) a b^(N-j).

Thus every codeword has length N + 4, begins with the synchronizing marker aa, and ends in b.

@[reducible, inline]

abbrev Undecidability.Thue.Matiyasevich1993.Binary.binaryLetterA : Fin 2

The first letter of the binary alphabet used in the first coding stage.

Equations

• Undecidability.Thue.Matiyasevich1993.Binary.binaryLetterA = 0

@[reducible, inline]

abbrev Undecidability.Thue.Matiyasevich1993.Binary.binaryLetterB : Fin 2

The second letter of the binary alphabet used in the first coding stage.

Equations

• Undecidability.Thue.Matiyasevich1993.Binary.binaryLetterB = 1

def Undecidability.Thue.Matiyasevich1993.Binary.rho₁Letter (N : ℕ) (j : Fin N) : List (Fin 2)

The letter code ρ₁(a_j) from (18), with j represented zero-based.

Equations

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

def Undecidability.Thue.Matiyasevich1993.Binary.rho₁ (N : ℕ) (W : List (Fin N)) : List (Fin 2)

The homomorphic extension of ρ₁ to words.

Equations

• Undecidability.Thue.Matiyasevich1993.Binary.rho₁ N W = List.flatMap (Undecidability.Thue.Matiyasevich1993.Binary.rho₁Letter N) W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Binary.rho₁_cons {N : ℕ} (j : Fin N) (W : List (Fin N)) : rho₁ N (j :: W) = rho₁Letter N j ++ rho₁ N W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Binary.rho₁_append {N : ℕ} (X Y : List (Fin N)) : rho₁ N (X ++ Y) = rho₁ N X ++ rho₁ N Y

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Binary.rho₁Letter_length {N : ℕ} (j : Fin N) : (rho₁Letter N j).length = N + 4

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Binary.rho₁_length {N : ℕ} (W : List (Fin N)) : (rho₁ N W).length = W.length * (N + 4)

theorem Undecidability.Thue.Matiyasevich1993.Binary.rho₁_computable (N : ℕ) : Computable (rho₁ N)

def Undecidability.Thue.Matiyasevich1993.Binary.indexRun (W : List (Fin 2)) : ℕ

Read the length of the first b-run after the initial marker.

Equations

• Undecidability.Thue.Matiyasevich1993.Binary.indexRun W = (List.takeWhile (fun (x : Fin 2) => x == Undecidability.Thue.Matiyasevich1993.Binary.binaryLetterB) (List.drop 2 W)).length

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Binary.indexRun_rho₁Letter {N : ℕ} (j : Fin N) : indexRun (rho₁Letter N j) = ↑j + 1

theorem Undecidability.Thue.Matiyasevich1993.Binary.rho₁Letter_injective {N : ℕ} : Function.Injective (rho₁Letter N)

theorem Undecidability.Thue.Matiyasevich1993.Binary.rho₁Letter_ends_b {N : ℕ} (j : Fin N) : ∃ (init : List (Fin 2)), rho₁Letter N j = init ++ [1]

theorem Undecidability.Thue.Matiyasevich1993.Binary.rho₁_injective {N : ℕ} : Function.Injective (rho₁ N)

theorem Undecidability.Thue.Matiyasevich1993.Binary.rho₁_starts_aa {N : ℕ} {W : List (Fin N)} (hW : W ≠ []) : ∃ (tail : List (Fin 2)), rho₁ N W = 0 :: 0 :: tail

Every nonempty encoded word begins with the synchronizing marker.

theorem Undecidability.Thue.Matiyasevich1993.Binary.rho₁_noAAA {N : ℕ} (W : List (Fin N)) : ¬∃ (l : List (Fin 2)) (s : List (Fin 2)), rho₁ N W = l ++ [0, 0, 0] ++ s

The code language contains no run aaa.

def Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeF {N r : ℕ} (F : Fin r → List (Fin N)) (i : Fin r) : List (Fin 2)

The two sides of the binary system T₂'.

Equations

• Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeF F i = Undecidability.Thue.Matiyasevich1993.Binary.rho₁ N (F i)

def Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeE {N r : ℕ} (E : Fin r → List (Fin N)) (i : Fin r) : List (Fin 2)

The right-hand rule words after the first binary alphabet encoding.

Equations

• Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeE E i = Undecidability.Thue.Matiyasevich1993.Binary.rho₁ N (E i)

def Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeSystem {N r : ℕ} (F E : Fin r → List (Fin N)) : ThueSystem (Fin 2)

The Thue system obtained by applying the first binary alphabet encoding to all rules.

Equations

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

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeF_length {N r : ℕ} (F : Fin r → List (Fin N)) (i : Fin r) : (stage₂PrimeF F i).length = (F i).length * (N + 4)

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeE_length {N r : ℕ} (E : Fin r → List (Fin N)) (i : Fin r) : (stage₂PrimeE E i).length = (E i).length * (N + 4)

theorem Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeF_common_length {N r : ℕ} (F : Fin r → List (Fin N)) (p : ℕ) (hF : ∀ (i : Fin r), (F i).length = p) (i : Fin r) : (stage₂PrimeF F i).length = p * (N + 4)

Common source-side lengths become common binary-side lengths.

theorem Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeE_common_length {N r : ℕ} (E : Fin r → List (Fin N)) (q : ℕ) (hE : ∀ (i : Fin r), (E i).length = q) (i : Fin r) : (stage₂PrimeE E i).length = q * (N + 4)

theorem Undecidability.Thue.Matiyasevich1993.Binary.decode_step {N r : ℕ} (F E : Fin r → List (Fin N)) (hF : ∀ (i : Fin r), F i ≠ []) (hE : ∀ (i : Fin r), E i ≠ []) {X : List (Fin N)} {W : List (Fin 2)} (h : ThueStep (stage₂PrimeSystem F E) (rho₁ N X) W) : ∃ (Y : List (Fin N)), W = rho₁ N Y ∧ ThueStep (finiteSystem F E) X Y

A rewrite out of an encoded word is aligned and uniquely reflects to one source rewrite. Positivity of all rule sides is the only hypothesis.

theorem Undecidability.Thue.Matiyasevich1993.Binary.decode_thueEq {N r : ℕ} (F E : Fin r → List (Fin N)) (hF : ∀ (i : Fin r), F i ≠ []) (hE : ∀ (i : Fin r), E i ≠ []) {X : List (Fin N)} {W : List (Fin 2)} (h : ThueEq (stage₂PrimeSystem F E) (rho₁ N X) W) : ∃ (Y : List (Fin N)), W = rho₁ N Y ∧ ThueEq (finiteSystem F E) X Y

Every derivation starting at an encoded word stays encoded and reflects to a source derivation.

theorem Undecidability.Thue.Matiyasevich1993.Binary.thueEq_iff {N r : ℕ} (F E : Fin r → List (Fin N)) (hF : ∀ (i : Fin r), F i ≠ []) (hE : ∀ (i : Fin r), E i ≠ []) (X Y : List (Fin N)) : ThueEq (finiteSystem F E) X Y ↔ ThueEq (stage₂PrimeSystem F E) (rho₁ N X) (rho₁ N Y)

Equivalence (19): the binary many-rule system is equivalent to the positive-side source system on encoded words.

def Undecidability.Thue.Matiyasevich1993.Binary.embedding {N r : ℕ} (F E : Fin r → List (Fin N)) (p q : ℕ) (hp : 0 < p) (hq : 0 < q) (hF : ∀ (i : Fin r), (F i).length = p) (hE : ∀ (i : Fin r), (E i).length = q) : Embedding (finiteSystem F E) (stage₂PrimeSystem F E)

Section 2.3 packaged as an Embedding, under the common positive side length hypotheses supplied by the padding stage.

Equations

• Undecidability.Thue.Matiyasevich1993.Binary.embedding F E p q hp hq hF hE = { encode := Undecidability.Thue.Matiyasevich1993.Binary.rho₁ N, encode_computable := ⋯, thueEq_iff := ⋯ }