Configurations as words: the rewriting system of a machine

The middle layer of the RE-hardness of DescriptiveComplexity.PCP: a machine on the unbounded tape of DescriptiveComplexity.MachinesUnbounded accepts exactly when the string-rewriting system read off its transition table derives the halting word from the start word (DescriptiveComplexity.HaltPcp.acceptsU_iff_derives). Composed with DescriptiveComplexity.Pcp.History.hasMatch_iff one file up, this makes the domino system of the machine decide its acceptance; the sibling Interp file draws that domino system as a first-order interpretation.

The words

A configuration is written as a word over DescriptiveComplexity.HaltPcp.TapeLetter: a left endmarker, the symbols of a finite window of consecutive tape cells with the state letter wedged in front of the head's cell, and a right endmarker (DescriptiveComplexity.HaltPcp.Represents). The window must contain the head and every non-blank cell, and may contain any amount of blank padding beyond them – a configuration has many words, which is what lets the rules extend the window on demand.

The format is kept strict: the state letter always has a symbol letter to its right (the cell the head is on). Each rule of DescriptiveComplexity.HaltPcp.MRule preserves strictness on its own – the boundary variants of the two moves extend the window by one blank cell in the same rewriting step – so every word of a derivation between the boot and the halting letter is a configuration word, and the backward reading of a derivation is a plain case analysis on the rule applied.

The rules

• the two moves, each in a running variant and a boundary variant that writes a blank into the cell entering the window. A transition's attributes are relations, not functions, so the rules are indexed by the attribute values, with the transition existentially quantified in the side condition;
• boot: the start word carries a boot letter in the state slot, and a rule per start state replaces it. This is what lets the single start domino of the PCP construction serve a machine with several start states;
• halting: a rule per accepting state replaces the state letter by the halting letter, and two-letter erasers then melt the rest of the word away. Both sides of every rule are nonempty, as the domino construction requires – erasure consumes a neighbouring letter instead of producing the empty word.

No letter of a configuration word is a boot or halting letter, so the boot rule fires only on the start word and the erasers only after an accepting state was seen: the phases of a derivation cannot mix.

The alphabet

inductive DescriptiveComplexity.HaltPcp.TapeLetter (A : Type) : Type

The alphabet configurations are written in: the two endmarkers of the window, the boot letter standing in the state slot of the start word, the halting letter, and a symbol letter and a state letter per element of the machine.

• lft {A : Type} : TapeLetter A

  The left endmarker of the window.

• rgt {A : Type} : TapeLetter A

  The right endmarker of the window.

• boot {A : Type} : TapeLetter A

  The boot letter, in the state slot of the start word.

• halt {A : Type} : TapeLetter A

  The halting letter, the one-letter word a derivation must reach.

• sym {A : Type} : A → TapeLetter A

  The contents of a tape cell.

• state {A : Type} : A → TapeLetter A

  The current state, wedged before the head's cell.

def DescriptiveComplexity.HaltPcp.TapeLetter.isState {A : Type} : TapeLetter A → Bool

Being a state letter, as a Boolean – the alphabet has no decidable equality to offer, but the constructor is decidable on its own.

Equations

• (DescriptiveComplexity.HaltPcp.TapeLetter.state a).isState = true
• x✝.isState = false

theorem DescriptiveComplexity.HaltPcp.TapeLetter.absurd_of_ne {A : Type} {P : Prop} {a b : TapeLetter A} (h : a = b) (hne : a ≠ b := by simp) : P

A letter of the words below is never a boot or halting letter; this is the shape the case analyses need.

The rules

inductive DescriptiveComplexity.HaltPcp.MRule {A : Type} (M : TMData A) : List (TapeLetter A) → List (TapeLetter A) → Prop

The rewriting system of a machine: the two moves with their boundary variants, the boot rule, and the halting rule with its erasers. The transition performing a move is existentially quantified in the side condition, since its attributes are relations rather than functions; the letters of the rule are the attribute values themselves.

• boot {A : Type} {M : TMData A} {q : A} : M.Start q → MRule M [TapeLetter.boot] [TapeLetter.state q]

  The boot letter becomes a start state.

• moveR {A : Type} {M : TMData A} {τ q a b q' c : A} : M.Tr τ → M.Right τ → M.Src τ q → M.Read τ a → M.Dst τ q' → M.Write τ b → MRule M [TapeLetter.state q, TapeLetter.sym a, TapeLetter.sym c] [TapeLetter.sym b, TapeLetter.state q', TapeLetter.sym c]

  A right move with the head staying inside the window: the letter beyond the head is carried along unchanged.

• moveREnd {A : Type} {M : TMData A} {τ q a b q' bk : A} : M.Tr τ → M.Right τ → M.Src τ q → M.Read τ a → M.Dst τ q' → M.Write τ b → M.Blank bk → MRule M [TapeLetter.state q, TapeLetter.sym a, TapeLetter.rgt] [TapeLetter.sym b, TapeLetter.state q', TapeLetter.sym bk, TapeLetter.rgt]

  A right move at the right edge of the window: the cell entering the window is blank.

• moveL {A : Type} {M : TMData A} {τ q a b q' c : A} : M.Tr τ → ¬M.Right τ → M.Src τ q → M.Read τ a → M.Dst τ q' → M.Write τ b → MRule M [TapeLetter.sym c, TapeLetter.state q, TapeLetter.sym a] [TapeLetter.state q', TapeLetter.sym c, TapeLetter.sym b]

  A left move with the head staying inside the window.

• moveLEnd {A : Type} {M : TMData A} {τ q a b q' bk : A} : M.Tr τ → ¬M.Right τ → M.Src τ q → M.Read τ a → M.Dst τ q' → M.Write τ b → M.Blank bk → MRule M [TapeLetter.lft, TapeLetter.state q, TapeLetter.sym a] [TapeLetter.lft, TapeLetter.state q', TapeLetter.sym bk, TapeLetter.sym b]

  A left move at the left edge of the window: the cell entering the window is blank.

• acc {A : Type} {M : TMData A} {q : A} : M.Acc q → MRule M [TapeLetter.state q] [TapeLetter.halt]

  An accepting state becomes the halting letter.

• eraseSymL {A : Type} {M : TMData A} (c : A) : MRule M [TapeLetter.sym c, TapeLetter.halt] [TapeLetter.halt]

  The halting letter swallows the symbol to its left.

• eraseLft {A : Type} {M : TMData A} : MRule M [TapeLetter.lft, TapeLetter.halt] [TapeLetter.halt]

  The halting letter swallows the left endmarker.

• eraseSymR {A : Type} {M : TMData A} (c : A) : MRule M [TapeLetter.halt, TapeLetter.sym c] [TapeLetter.halt]

  The halting letter swallows the symbol to its right.

• eraseRgt {A : Type} {M : TMData A} : MRule M [TapeLetter.halt, TapeLetter.rgt] [TapeLetter.halt]

  The halting letter swallows the right endmarker.

theorem DescriptiveComplexity.HaltPcp.mRule_ne {A : Type} {M : TMData A} {l r : List (TapeLetter A)} (h : MRule M l r) : l ≠ [] ∧ r ≠ []

No side of a rule is empty – the promise the domino construction requires.

The order of the cells

The cells ℤ × A are ordered lexicographically – pages first, the machine's order on the offsets inside a page – and one DescriptiveComplexity.TMData.SuccCell step increases that order strictly. This is what makes a window a duplicate-free list and puts a cell entering it outside of it.

def DescriptiveComplexity.HaltPcp.CellLt {A : Type} (M : TMData A) (x y : ℤ × A) : Prop

The strict lexicographic order on cells.

Equations

• DescriptiveComplexity.HaltPcp.CellLt M x y = (x.1 < y.1 ∨ x.1 = y.1 ∧ M.Le x.2 y.2 ∧ x.2 ≠ y.2)

theorem DescriptiveComplexity.HaltPcp.CellLt.trans {A : Type} {M : TMData A} (hlin : IsLinOrd M.Le) {x y z : ℤ × A} (hxy : CellLt M x y) (hyz : CellLt M y z) : CellLt M x z

theorem DescriptiveComplexity.HaltPcp.CellLt.ne {A : Type} {M : TMData A} {x y : ℤ × A} (h : CellLt M x y) : x ≠ y

theorem DescriptiveComplexity.HaltPcp.cellLt_of_succCell {A : Type} {M : TMData A} {x y : ℤ × A} (h : M.SuccCell x y) : CellLt M x y

theorem DescriptiveComplexity.HaltPcp.pairwise_cellLt_of_isChain {A : Type} {M : TMData A} (hlin : IsLinOrd M.Le) {l : List (ℤ × A)} : List.IsChain M.SuccCell l → List.Pairwise (CellLt M) l

A chain of successive cells is duplicate-free and increasing.

Every cell has a next one and a previous one

On a well-formed machine with at least one position, the strip of pages is unbounded in both directions: the mirror-image lemmas of DescriptiveComplexity.exists_predPos supply the missing successor facts.

theorem DescriptiveComplexity.HaltPcp.succPos_reverse {A : Type} {Le : A → A → Prop} {Posn : A → Prop} {p q : A} : SuccPos (fun (a b : A) => Le b a) Posn p q ↔ SuccPos Le Posn q p

SuccPos mirrors along the reversed order.

theorem DescriptiveComplexity.HaltPcp.exists_succPos {A : Type} [Finite A] {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {p : A} (hp : Posn p) (hmax : ¬MaxPos Le Posn p) : ∃ (q : A), SuccPos Le Posn p q

Every position that is not the highest has one immediately above it.

theorem DescriptiveComplexity.HaltPcp.exists_succCell {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {x : ℤ × A} (hx : M.Posn x.2) : ∃ (y : ℤ × A), M.SuccCell x y

Every cell over a position has a next cell.

theorem DescriptiveComplexity.HaltPcp.exists_predCell {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {x : ℤ × A} (hx : M.Posn x.2) : ∃ (y : ℤ × A), M.SuccCell y x

Every cell over a position has a previous cell.

theorem DescriptiveComplexity.HaltPcp.minPos_unique {A : Type} {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {p q : A} (hp : MinPos Le Posn p) (hq : MinPos Le Posn q) : p = q

Lowest positions are unique.

theorem DescriptiveComplexity.HaltPcp.maxPos_unique {A : Type} {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {p q : A} (hp : MaxPos Le Posn p) (hq : MaxPos Le Posn q) : p = q

Highest positions are unique.

theorem DescriptiveComplexity.HaltPcp.succPos_right_unique {A : Type} {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {p q q' : A} (h : SuccPos Le Posn p q) (h' : SuccPos Le Posn p q') : q = q'

The element immediately above a given one is unique.

theorem DescriptiveComplexity.HaltPcp.succPos_not_maxPos {A : Type} {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {p q : A} (h : SuccPos Le Posn p q) : ¬MaxPos Le Posn p

A position with a successor is not the highest.

theorem DescriptiveComplexity.HaltPcp.succPos_not_minPos {A : Type} {Le : A → A → Prop} {Posn : A → Prop} (hlin : IsLinOrd Le) {p q : A} (h : SuccPos Le Posn p q) : ¬MinPos Le Posn q

A position with a predecessor is not the lowest.

theorem DescriptiveComplexity.HaltPcp.succCell_right_unique {A : Type} {M : TMData A} (hwf : M.WellFormed) {x y y' : ℤ × A} (h : M.SuccCell x y) (h' : M.SuccCell x y') : y = y'

The cell after a given one is unique.

theorem DescriptiveComplexity.HaltPcp.succCell_left_unique {A : Type} {M : TMData A} (hwf : M.WellFormed) {x x' y : ℤ × A} (h : M.SuccCell x y) (h' : M.SuccCell x' y) : x = x'

The cell before a given one is unique.

theorem DescriptiveComplexity.HaltPcp.posn_of_succCell {A : Type} {M : TMData A} {x y : ℤ × A} (h : M.SuccCell x y) : M.Posn y.2

The successor cell keeps to the positions.

theorem DescriptiveComplexity.HaltPcp.posn_of_succCell_left {A : Type} {M : TMData A} {x y : ℤ × A} (h : M.SuccCell x y) : M.Posn x.2

The previous cell keeps to the positions, too.

Configuration words

A configuration is written as a window of consecutive cells: the symbols they hold, with the state letter wedged before the head's cell and an endmarker at each end. The window contains the head and every non-blank cell over a position; it may contain blank padding beyond them, so a configuration has many words.

def DescriptiveComplexity.HaltPcp.cellSyms {A : Type} (c : ConfigU A) (l : List (ℤ × A)) : List (TapeLetter A)

The symbol letters of a list of cells.

Equations

• DescriptiveComplexity.HaltPcp.cellSyms c l = List.map (fun (x : ℤ × A) => DescriptiveComplexity.HaltPcp.TapeLetter.sym (c.tape x)) l

@[simp]

theorem DescriptiveComplexity.HaltPcp.cellSyms_nil {A : Type} (c : ConfigU A) : cellSyms c [] = []

@[simp]

theorem DescriptiveComplexity.HaltPcp.cellSyms_cons {A : Type} (c : ConfigU A) (x : ℤ × A) (l : List (ℤ × A)) : cellSyms c (x :: l) = TapeLetter.sym (c.tape x) :: cellSyms c l

@[simp]

theorem DescriptiveComplexity.HaltPcp.cellSyms_append {A : Type} (c : ConfigU A) (l l' : List (ℤ × A)) : cellSyms c (l ++ l') = cellSyms c l ++ cellSyms c l'

theorem DescriptiveComplexity.HaltPcp.cellSyms_congr {A : Type} {c c' : ConfigU A} {l : List (ℤ × A)} (h : ∀ x ∈ l, c'.tape x = c.tape x) : cellSyms c' l = cellSyms c l

Two configurations agreeing on a window write it the same way.

def DescriptiveComplexity.HaltPcp.Represents {A : Type} (M : TMData A) (w : List (TapeLetter A)) (c : ConfigU A) : Prop

w is a word of the configuration c: the symbols of a window of consecutive cells between the two endmarkers, the state letter wedged before the head's cell. The window consists of cells over positions, contains the head, and every cell over a position outside it is blank.

Equations

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

Letters of a configuration word

A configuration word carries no boot and no halting letter, and exactly one state letter; these two facts drive the case analysis on a rewriting step.

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_lft {A : Type} : TapeLetter.lft.isState = false

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_rgt {A : Type} : TapeLetter.rgt.isState = false

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_boot {A : Type} : TapeLetter.boot.isState = false

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_halt {A : Type} : TapeLetter.halt.isState = false

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_sym {A : Type} (a : A) : (TapeLetter.sym a).isState = false

@[simp]

theorem DescriptiveComplexity.HaltPcp.isState_state {A : Type} (q : A) : (TapeLetter.state q).isState = true

def DescriptiveComplexity.HaltPcp.stateCount {A : Type} (l : List (TapeLetter A)) : ℕ

The number of state letters of a word.

Equations

• DescriptiveComplexity.HaltPcp.stateCount l = List.countP DescriptiveComplexity.HaltPcp.TapeLetter.isState l

@[simp]

theorem DescriptiveComplexity.HaltPcp.stateCount_nil {A : Type} : stateCount [] = 0

theorem DescriptiveComplexity.HaltPcp.stateCount_append {A : Type} (l l' : List (TapeLetter A)) : stateCount (l ++ l') = stateCount l + stateCount l'

theorem DescriptiveComplexity.HaltPcp.stateCount_cons {A : Type} (a : TapeLetter A) (l : List (TapeLetter A)) : stateCount (a :: l) = stateCount l + if a.isState = true then 1 else 0

@[simp]

theorem DescriptiveComplexity.HaltPcp.stateCount_cellSyms {A : Type} (c : ConfigU A) (l : List (ℤ × A)) : stateCount (cellSyms c l) = 0

theorem DescriptiveComplexity.HaltPcp.stateCount_eq_zero {A : Type} {l : List (TapeLetter A)} : stateCount l = 0 ↔ ∀ x ∈ l, x.isState = false

A word without state letters is exactly a word of vanishing state count.

theorem DescriptiveComplexity.HaltPcp.state_align {A : Type} {u₁ u₂ v₁ v₂ : List (TapeLetter A)} {q₁ q₂ : A} : u₁ ++ TapeLetter.state q₁ :: v₁ = u₂ ++ TapeLetter.state q₂ :: v₂ → (∀ x ∈ u₁, x.isState = false) → (∀ x ∈ u₂, x.isState = false) → u₁ = u₂ ∧ q₁ = q₂ ∧ v₁ = v₂

Alignment at the state letter: two decompositions of one word around a state letter, neither prefix carrying one, agree.

theorem DescriptiveComplexity.HaltPcp.prefix_state_free {A : Type} (c : ConfigU A) (ls : List (ℤ × A)) (x : TapeLetter A) : x ∈ TapeLetter.lft :: cellSyms c ls → x.isState = false

The prefix of a configuration word carries no state letter.

theorem DescriptiveComplexity.HaltPcp.boot_halt_notMem {A : Type} {M : TMData A} {w : List (TapeLetter A)} {c : ConfigU A} (h : Represents M w c) : TapeLetter.boot ∉ w ∧ TapeLetter.halt ∉ w

No boot letter and no halting letter occurs in a configuration word.

theorem DescriptiveComplexity.HaltPcp.window_lt {A : Type} {M : TMData A} {ls rs : List (ℤ × A)} {h : ℤ × A} (hlin : IsLinOrd M.Le) (hchain : List.IsChain M.SuccCell (ls ++ h :: rs)) : (∀ z ∈ ls, CellLt M z h) ∧ ∀ z ∈ rs, CellLt M h z

The two halves of a window sit strictly below and strictly above the head.

theorem DescriptiveComplexity.HaltPcp.stateCount_word {A : Type} (c : ConfigU A) (ls rs : List (ℤ × A)) : stateCount (TapeLetter.lft :: cellSyms c ls ++ TapeLetter.state c.state :: TapeLetter.sym (c.tape c.head) :: (cellSyms c rs ++ [TapeLetter.rgt])) = 1

A configuration word has exactly one state letter.

Reading a rewriting step off a configuration word

The inversion at the heart of the backward direction: a rewriting step on a configuration word either simulates one machine step or fires the halting rule on the current – hence accepting – state. Each move rule carries exactly one state letter on its left-hand side, and a configuration word carries exactly one, so the rule can only apply at the head.

theorem DescriptiveComplexity.HaltPcp.step_inversion {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {w w₁ : List (TapeLetter A)} {c : ConfigU A} (hrep : Represents M w c) (hstep : Pcp.History.Step (MRule M) w w₁) : (∃ (c' : ConfigU A), M.StepU c c' ∧ Represents M w₁ c') ∨ M.Acc c.state

Writing a machine step as a rewriting step

The forward direction: one machine step is one rewriting step – the boundary variants of the moves extend the window in the same stroke, so no separate padding step is ever needed.

theorem DescriptiveComplexity.HaltPcp.exists_step_of_stepU {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {w : List (TapeLetter A)} {c c' : ConfigU A} (hrep : Represents M w c) (h : M.StepU c c') : ∃ (w' : List (TapeLetter A)), Pcp.History.Step (MRule M) w w' ∧ Represents M w' c'

Whole runs, and the halting phase

theorem DescriptiveComplexity.HaltPcp.derives_of_run {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {n : ℕ} {c c' : ConfigU A} : M.StepsInU n c c' → ∀ {w : List (TapeLetter A)}, Represents M w c → ∃ (w' : List (TapeLetter A)), Pcp.History.Derives (MRule M) w w' ∧ Represents M w' c'

A run of the machine is a derivation between words of its endpoints.

theorem DescriptiveComplexity.HaltPcp.derives_eraseL {A : Type} {M : TMData A} (u : List A) : Pcp.History.Derives (MRule M) (List.map TapeLetter.sym u ++ [TapeLetter.halt]) [TapeLetter.halt]

The halting letter melts a block of symbols to its left away.

theorem DescriptiveComplexity.HaltPcp.derives_eraseR {A : Type} {M : TMData A} (u : List A) : Pcp.History.Derives (MRule M) (TapeLetter.halt :: List.map TapeLetter.sym u) [TapeLetter.halt]

The halting letter melts a block of symbols to its right away.

theorem DescriptiveComplexity.HaltPcp.derives_halt_of_acc {A : Type} {M : TMData A} {w : List (TapeLetter A)} {c : ConfigU A} (hrep : Represents M w c) (hacc : M.Acc c.state) : Pcp.History.Derives (MRule M) w [TapeLetter.halt]

From an accepting configuration the derivation closes: the state letter becomes the halting letter, which then swallows the whole word.

The start word

The start word writes the input page between the endmarkers, with the boot letter in the state slot; the boot rule turns it into a word of an initial configuration. The page is read along an enumeration of the positions in the machine's order.

def DescriptiveComplexity.HaltPcp.IsPosEnum {A : Type} (M : TMData A) (ps : List A) : Prop

ps enumerates the positions, in the machine's order.

Equations

• DescriptiveComplexity.HaltPcp.IsPosEnum M ps = (List.Pairwise (fun (p q : A) => M.Le p q ∧ p ≠ q) ps ∧ ∀ (p : A), p ∈ ps ↔ M.Posn p)

def DescriptiveComplexity.HaltPcp.startWord {A : Type} (inp : List A) : List (TapeLetter A)

The start word of an input page: endmarkers, the boot letter, and the symbols of the page.

Equations

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

theorem DescriptiveComplexity.HaltPcp.IsPosEnum.ne_nil {A : Type} {M : TMData A} (hwf : M.WellFormed) {ps : List A} (hps : IsPosEnum M ps) : ps ≠ []

A machine with a position has a nonempty enumeration.

theorem DescriptiveComplexity.HaltPcp.IsPosEnum.isChain {A : Type} {M : TMData A} (hlin : IsLinOrd M.Le) {ps : List A} (hps : IsPosEnum M ps) : List.IsChain (SuccPos M.Le M.Posn) ps

Consecutive entries of an enumeration are consecutive positions.

theorem DescriptiveComplexity.HaltPcp.IsPosEnum.head_minPos {A : Type} {M : TMData A} (hlin : IsLinOrd M.Le) {p : A} {pr : List A} (hps : IsPosEnum M (p :: pr)) : MinPos M.Le M.Posn p

The first entry of an enumeration is the lowest position.

theorem DescriptiveComplexity.HaltPcp.exists_isInitU {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {q₀ : A} (hq : M.Start q₀) : ∃ (c₀ : ConfigU A), M.IsInitU c₀ ∧ c₀.state = q₀

A well-formed machine with a start state has an initial configuration on the unbounded tape, its input page filled by choice and the rest blank.

theorem DescriptiveComplexity.HaltPcp.represents_of_isInitU {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {ps inp : List A} (hps : IsPosEnum M ps) (hinp : List.Forall₂ M.InitTape ps inp) {c₀ : ConfigU A} (hinit : M.IsInitU c₀) : Represents M (TapeLetter.lft :: TapeLetter.state c₀.state :: (List.map TapeLetter.sym inp ++ [TapeLetter.rgt])) c₀

The word of an initial configuration: the input page between the endmarkers, the state in front of its first cell.

theorem DescriptiveComplexity.HaltPcp.stateCount_startWord {A : Type} (inp : List A) : stateCount (startWord inp) = 0

No letter of a start word is a state or halting letter, and its only boot letter is the one in the state slot.

The equivalence

theorem DescriptiveComplexity.HaltPcp.acceptsU_of_derives {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {w : List (TapeLetter A)} (hder : Pcp.History.Derives (MRule M) w [TapeLetter.halt]) (c : ConfigU A) : Represents M w c → ∃ (c' : ConfigU A) (n : ℕ), M.StepsInU n c c' ∧ M.Acc c'.state

The backward reading: a derivation from a configuration word to the halting word yields an accepting run from that configuration.

theorem DescriptiveComplexity.HaltPcp.acceptsU_iff_derives {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {ps inp : List A} (hps : IsPosEnum M ps) (hinp : List.Forall₂ M.InitTape ps inp) : M.AcceptsU ↔ Pcp.History.Derives (MRule M) (startWord inp) [TapeLetter.halt]

Acceptance is derivability: the machine accepts exactly when the rewriting system derives the halting word from the start word.

theorem DescriptiveComplexity.HaltPcp.acceptsU_iff_hasMatch {A : Type} {M : TMData A} [Finite A] (hwf : M.WellFormed) {ps inp : List A} (hps : IsPosEnum M ps) (hinp : List.Forall₂ M.InitTape ps inp) : M.AcceptsU ↔ Pcp.History.HasMatch (MRule M) (startWord inp) TapeLetter.halt

Acceptance is having a match: the domino system of the machine's rewriting rules has a match exactly when the machine accepts.