@[reducible, inline]

abbrev TuringMachine.CellSymbol (Q Γ : Type) : Type

A cell symbol that may appear in a single cell of a Cook-Levin tableau: either a tape symbol γ ∈ Γ (representing tape contents) or a state q ∈ Q (marking the head position together with the current state).

def TuringMachine.encodeConfigRow {Q Γ : Type} (c : Config Q Γ) (width : ℕ) : Fin width → CellSymbol Q Γ

Encode a TM configuration c as one row of a tableau of given width: position j holds the state c.state (as Sum.inl) if the head is over cell j, and otherwise the tape symbol c.tape j (as Sum.inr).

def TuringMachine.IsLegalWindow {Q Γ : Type} (M : NTM Q Γ) (a b c d e f : CellSymbol Q Γ) : Prop

IsLegalWindow M a b c d e f says that the 2 × 3 window

a b c
d e f

is consistent with one step of the NTM M: the top row (a, b, c) is the parent and the bottom row (d, e, f) is the child. There are two cases:

1. No head in the top window. If none of a, b, c is a state symbol, then the cell directly below b must equal b (the tape doesn't change away from the head).
2. Head at the centre. If b = ⟨q⟩ for some state q and the tape symbol above b is γ, then there must be some transition (q', γ', dir) ∈ M.δ q γ consistent with the bottom row, or the window may alternatively show no change (e = γ).

This is the local-consistency predicate used in the Cook-Levin tableau argument.

@[reducible, inline]

abbrev TuringMachine.IsLegalSextuple {Q Γ : Type} (M : NTM Q Γ) (a b c d e f : CellSymbol Q Γ) : Prop

Alternative name for IsLegalWindow: a legal 6-tuple (a, b, c, d, e, f) describing a 2×3 window.

structure TuringMachine.Tableau {Q Γ : Type} (M : NTM Q Γ) (w : List Γ) : Type

An (accepting) tableau for NTM M on input w. Following Sipser, this is an nᵏ × nᵏ table (where n = |w|) of CellSymbols representing a computation history on some accepting branch of M's nondeterministic computation:

• k — the polynomial exponent giving the table's side length.
• cell i j — the contents of row i, column j.
• size_pos — the side length nᵏ is positive.
• start — row 0 is the encoding of the initial configuration of M on w.
• accept — the last row contains the accept state somewhere.
• move — every interior 2 × 3 window is a legal window (IsLegalWindow M …), enforcing that consecutive rows describe valid computation steps of M.

The existence of such a tableau is the central object in the Cook-Levin proof that SAT (and 3SAT) are NP-complete.

• k : ℕ
• cell : Fin (w.length ^ self.k) → Fin (w.length ^ self.k) → CellSymbol Q Γ
• size_pos : 0 < w.length ^ self.k
• start : self.cell ⟨0, ⋯⟩ = encodeConfigRow (M.initConfig w) (w.length ^ self.k)
• accept : ∃ (j : Fin (w.length ^ self.k)), self.cell ⟨w.length ^ self.k - 1, ⋯⟩ j = Sum.inl M.qAccept
• move (i : Fin (w.length ^ self.k)) (hi : ↑i + 1 < w.length ^ self.k) (j : Fin (w.length ^ self.k)) (hj1 : 0 < ↑j) (hj2 : ↑j + 1 < w.length ^ self.k) : IsLegalWindow M (self.cell i ⟨↑j - 1, ⋯⟩) (self.cell i j) (self.cell i ⟨↑j + 1, hj2⟩) (self.cell ⟨↑i + 1, hi⟩ ⟨↑j - 1, ⋯⟩) (self.cell ⟨↑i + 1, hi⟩ j) (self.cell ⟨↑i + 1, hi⟩ ⟨↑j + 1, hj2⟩)