The first, padding, stage of Section 2.2 of Matiyasevich (1995). Starting from a finite system T₀, it adds one letter d and produces a system T₁ whose left sides all have one common positive length p, and whose right sides all have the common length q = p + 1.

def Undecidability.Thue.Matiyasevich1993.Padding.pad {n : ℕ} : Fin (n + 1)

The new letter a_{n+1} in the paper.

Equations

• Undecidability.Thue.Matiyasevich1993.Padding.pad = Fin.last n

def Undecidability.Thue.Matiyasevich1993.Padding.liftLetter {n : ℕ} (x : Fin n) : Fin (n + 1)

The inclusion A₀ ↪ A₁.

Equations

• Undecidability.Thue.Matiyasevich1993.Padding.liftLetter x = x.castSucc

def Undecidability.Thue.Matiyasevich1993.Padding.liftWord {n : ℕ} (W : List (Fin n)) : List (Fin (n + 1))

The homomorphic extension of liftLetter.

Equations

• Undecidability.Thue.Matiyasevich1993.Padding.liftWord W = List.map Undecidability.Thue.Matiyasevich1993.Padding.liftLetter W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.liftWord_append {n : ℕ} (X Y : List (Fin n)) : liftWord (X ++ Y) = liftWord X ++ liftWord Y

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.liftWord_length {n : ℕ} (W : List (Fin n)) : (liftWord W).length = W.length

def Undecidability.Thue.Matiyasevich1993.Padding.projectLetter {n : ℕ} (x : Fin (n + 1)) : Option (Fin n)

Delete every occurrence of the new padding letter. This is φ₀.

Equations

• Undecidability.Thue.Matiyasevich1993.Padding.projectLetter x = Fin.lastCases none some x

def Undecidability.Thue.Matiyasevich1993.Padding.decode {n : ℕ} (W : List (Fin (n + 1))) : List (Fin n)

The padding-stage decoder, which discards padding letters.

Equations

• Undecidability.Thue.Matiyasevich1993.Padding.decode W = List.filterMap Undecidability.Thue.Matiyasevich1993.Padding.projectLetter W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.projectLetter_pad {n : ℕ} : projectLetter pad = none

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.projectLetter_lift {n : ℕ} (x : Fin n) : projectLetter (liftLetter x) = some x

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.decode_append {n : ℕ} (X Y : List (Fin (n + 1))) : decode (X ++ Y) = decode X ++ decode Y

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.decode_liftWord {n : ℕ} (W : List (Fin n)) : decode (liftWord W) = W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.decode_replicate_pad {n : ℕ} (k : ℕ) : decode (List.replicate k pad) = []

def Undecidability.Thue.Matiyasevich1993.Padding.sideBound {n r : ℕ} (F E : Fin r → List (Fin n)) : ℕ

A computable upper bound for every source-rule side length.

Equations

• Undecidability.Thue.Matiyasevich1993.Padding.sideBound F E = List.foldr max 0 (List.ofFn fun (i : Fin r) => max (F i).length (E i).length)

def Undecidability.Thue.Matiyasevich1993.Padding.p {n r : ℕ} (F E : Fin r → List (Fin n)) : ℕ

The common length of the left sides of T₁.

Equations

• Undecidability.Thue.Matiyasevich1993.Padding.p F E = Undecidability.Thue.Matiyasevich1993.Padding.sideBound F E + 1

def Undecidability.Thue.Matiyasevich1993.Padding.q {n r : ℕ} (F E : Fin r → List (Fin n)) : ℕ

The common length of the right sides of T₁.

Equations

• Undecidability.Thue.Matiyasevich1993.Padding.q F E = Undecidability.Thue.Matiyasevich1993.Padding.p F E + 1

theorem Undecidability.Thue.Matiyasevich1993.Padding.F_length_lt_p {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin r) : (F i).length < p F E

theorem Undecidability.Thue.Matiyasevich1993.Padding.E_length_lt_p {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin r) : (E i).length < p F E

theorem Undecidability.Thue.Matiyasevich1993.Padding.p_pos {n r : ℕ} (F E : Fin r → List (Fin n)) : 0 < p F E

theorem Undecidability.Thue.Matiyasevich1993.Padding.p_le_q {n r : ℕ} (F E : Fin r → List (Fin n)) : p F E ≤ q F E

def Undecidability.Thue.Matiyasevich1993.Padding.stage₁F {n r : ℕ} (F E : Fin r → List (Fin n)) : Fin (r + (n + 1)) → List (Fin (n + 1))

Relations (16) and the left sides of relations (17).

Equations

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

def Undecidability.Thue.Matiyasevich1993.Padding.stage₁E {n r : ℕ} (F E : Fin r → List (Fin n)) : Fin (r + (n + 1)) → List (Fin (n + 1))

Relations (16) and the right sides of relations (17).

Equations

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

def Undecidability.Thue.Matiyasevich1993.Padding.stage₁System {n r : ℕ} (F E : Fin r → List (Fin n)) : ThueSystem (Fin (n + 1))

The Thue system obtained by adjoining padding letters and padding-stage rules.

Equations

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

def Undecidability.Thue.Matiyasevich1993.Padding.encode {n r : ℕ} (F E : Fin r → List (Fin n)) (W : List (Fin n)) : List (Fin (n + 1))

τ₀(G) = ρ₀(G)d^q, equation (11) for the first stage.

Equations

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

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.decode_encode {n r : ℕ} (F E : Fin r → List (Fin n)) (W : List (Fin n)) : decode (encode F E W) = W

theorem Undecidability.Thue.Matiyasevich1993.Padding.encode_computable {n r : ℕ} (F E : Fin r → List (Fin n)) : Computable (encode F E)

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.stage₁F_primary {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin r) : stage₁F F E (Fin.castAdd (n + 1) i) = liftWord (F i) ++ List.replicate (p F E - (F i).length) pad

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.stage₁E_primary {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin r) : stage₁E F E (Fin.castAdd (n + 1) i) = liftWord (E i) ++ List.replicate (q F E - (E i).length) pad

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.stage₁F_shift {n r : ℕ} (F E : Fin r → List (Fin n)) (j : Fin (n + 1)) : stage₁F F E (Fin.natAdd r j) = [j] ++ List.replicate (p F E - 1) pad

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Padding.stage₁E_shift {n r : ℕ} (F E : Fin r → List (Fin n)) (j : Fin (n + 1)) : stage₁E F E (Fin.natAdd r j) = [pad, j] ++ List.replicate (q F E - 2) pad

theorem Undecidability.Thue.Matiyasevich1993.Padding.stage₁F_length {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (r + (n + 1))) : (stage₁F F E i).length = p F E

theorem Undecidability.Thue.Matiyasevich1993.Padding.stage₁E_length {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (r + (n + 1))) : (stage₁E F E i).length = q F E

theorem Undecidability.Thue.Matiyasevich1993.Padding.simulate_step {n r : ℕ} (F E : Fin r → List (Fin n)) {X Y : List (Fin n)} (h : ThueStep (finiteSystem F E) X Y) : ThueEq (stage₁System F E) (encode F E X) (encode F E Y)

Forward simulation of one arbitrary T₀ step.

theorem Undecidability.Thue.Matiyasevich1993.Padding.simulate {n r : ℕ} (F E : Fin r → List (Fin n)) {X Y : List (Fin n)} (h : ThueEq (finiteSystem F E) X Y) : ThueEq (stage₁System F E) (encode F E X) (encode F E Y)

Forward half of equivalence (10) for all derivations.

theorem Undecidability.Thue.Matiyasevich1993.Padding.decode_step {n r : ℕ} (F E : Fin r → List (Fin n)) {X Y : List (Fin (n + 1))} (h : ThueStep (stage₁System F E) X Y) : ThueEq (finiteSystem F E) (decode X) (decode Y)

Every first-stage rewrite decodes either to one source rewrite or to an identity. This is the argument in the last paragraph of Section 2.2.

theorem Undecidability.Thue.Matiyasevich1993.Padding.decode_thueEq {n r : ℕ} (F E : Fin r → List (Fin n)) {X Y : List (Fin (n + 1))} (h : ThueEq (stage₁System F E) X Y) : ThueEq (finiteSystem F E) (decode X) (decode Y)

φ₀ maps an entire first-stage derivation to a source derivation.

theorem Undecidability.Thue.Matiyasevich1993.Padding.reflect {n r : ℕ} (F E : Fin r → List (Fin n)) {X Y : List (Fin n)} (h : ThueEq (stage₁System F E) (encode F E X) (encode F E Y)) : ThueEq (finiteSystem F E) X Y

Reflection half of equivalence (10) for the padding stage.

def Undecidability.Thue.Matiyasevich1993.Padding.embedding {n r : ℕ} (F E : Fin r → List (Fin n)) : Embedding (finiteSystem F E) (stage₁System F E)

The complete first-stage instance of equivalence (10).

Equations

• Undecidability.Thue.Matiyasevich1993.Padding.embedding F E = { encode := Undecidability.Thue.Matiyasevich1993.Padding.encode F E, encode_computable := ⋯, thueEq_iff := ⋯ }