Core

Part of the dependency closure of the small undecidable group constructions.

@[reducible, inline]

abbrev Undecidability.ThueSystem (α : Type u_1) : Type u_1

A finite-word Thue system, regarded as a symmetric rewriting system.

Equations

• Undecidability.ThueSystem α = Set (List α × List α)

def Undecidability.ThueStep {α : Type u_1} (T : ThueSystem α) (u v : List α) : Prop

One application of a Thue rule in an arbitrary two-sided context.

Equations

• Undecidability.ThueStep T u v = ∃ (l : List α) (r : List α) (x : List α) (y : List α), (x, y) ∈ T ∧ (u = l ++ x ++ r ∧ v = l ++ y ++ r ∨ u = l ++ y ++ r ∧ v = l ++ x ++ r)

def Undecidability.ThueEq {α : Type u_1} (T : ThueSystem α) (a : List α) : List α → Prop

Equality generated by finitely many Thue rewrites.

Equations

• Undecidability.ThueEq T = Relation.ReflTransGen (Undecidability.ThueStep T)

theorem Undecidability.Thue.thueStep_symm {α : Type u_1} {T : ThueSystem α} {X Y : List α} (h : ThueStep T X Y) : ThueStep T Y X

theorem Undecidability.Thue.thueEq_symm {α : Type u_1} {T : ThueSystem α} {X Y : List α} (h : ThueEq T X Y) : ThueEq T Y X

theorem Undecidability.Thue.thueStep_context {α : Type u_1} {T : ThueSystem α} (l r : List α) {X Y : List α} (h : ThueStep T X Y) : ThueStep T (l ++ X ++ r) (l ++ Y ++ r)

theorem Undecidability.Thue.thueEq_context {α : Type u_1} {T : ThueSystem α} (l r : List α) {X Y : List α} (h : ThueEq T X Y) : ThueEq T (l ++ X ++ r) (l ++ Y ++ r)

def Undecidability.Thue.baseF (U₃ : List (Fin 2)) : Fin 3 → List (Fin 2)

The three left sides before applying the synchronizing code.

Equations

• Undecidability.Thue.baseF U₃ = ![[0, 0, 1, 0, 1], [0, 0, 1, 1], U₃]

def Undecidability.Thue.baseE (V₃ : List (Fin 2)) : Fin 3 → List (Fin 2)

The three right sides before applying the synchronizing code.

Equations

• Undecidability.Thue.baseE V₃ = ![[1, 0, 0], [1, 0, 0], V₃]

def Undecidability.Thue.baseSystem (U₃ V₃ : List (Fin 2)) : ThueSystem (Fin 2)

The binary three-rule Thue system parametrized by its long left and right words.

Equations

• Undecidability.Thue.baseSystem U₃ V₃ = Set.range fun (i : Fin 3) => (Undecidability.Thue.baseF U₃ i, Undecidability.Thue.baseE V₃ i)