Part 9 of 9
TheoremThe five Cook–Levin clause families are satisfiable iff some certificate is accepted#✓fully proved
Let \(E\) be an encoding of the multi-stack machine \(M\), with input stack \(k_0\), output stack \(k_1\) and window depth \(d\). Let \(x\) and \(Y\) be lists of input symbols, let \(m, T \in \mathbb{N}\), let \(\mathrm{acc}\) be an output symbol, and let \(H = m + (T + 1)d + 1\) be the stack cap. Suppose \(|x| \le m\) and \(\mathrm{acc}\) is one of the effective symbols that \(E\) fixes for stack \(k_1\). Then some list \(a\) of Booleans satisfies all five of the following CNF formulas, each for \(T\) steps and cap \(H\): the transition family with tables \(\mathrm{la}, \mathrm{na}, \mathrm{wa}\) and the transition family with tables \(\mathrm{la}, \mathrm{sa}, \mathrm{wa}\), both over the layout of \(E\) and its \(N\) situations; the cell-shift family over the same layout with tables \(\mathrm{sa}, \mathrm{pl}, \mathrm{cn}, \mathrm{pu}\) and \(N\) situations; the init family for \(x\), \(Y\) and \(m\); and the accept family for \(\mathrm{acc}\), if and only if there is a list \(y\) of input symbols, all in \(Y\), with \(|xy| \le m\) such that the idle-extended run of \(M\) from the initial configuration on input \(xy\) is, after \(T\) steps, an accepting configuration for \(\mathrm{acc}\): halted, in the initial state, with \(\mathrm{acc}\) on top of stack \(k_1\).
theorem five_iff {x Ys : List (M.Γ M.k₀)} {m T : ℕ} {acc : M.Γ M.k₁}
(hx : x.length ≤ m) (hacc : ∃ i, E.dec M.k₁ i = acc) :
(∃ a : List Bool,
cnfSat (Family.family E.layout E.la E.na E.wa T (capH m T (depth M)) E.N) a ∧
cnfSat (Family.family E.layout E.la E.sa E.wa T (capH m T (depth M)) E.N) a ∧
cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T (capH m T (depth M))) a ∧
cnfSat (E.initFamily x Ys m T (capH m T (depth M))) a ∧
cnfSat (E.accFamily acc T (capH m T (depth M))) a) ↔
∃ y : List (M.Γ M.k₀), (∀ z ∈ y, z ∈ Ys) ∧ (x ++ y).length ≤ m ∧
Accepts M (runI M (initList M (x ++ y)) T) accdef cnfSat (φ : CNF) (a : List Bool) : Prop :=
∀ c ∈ φ, clauseSat c aCSLibExt/Computability/Complexity/DenseSAT.lean:67
def family (T H N : ℕ) : CNF :=
(List.range T).flatMap fun t =>
(List.range N).map fun i => denseClause (L.numVars T H) (lits L la na wa H t i)CSLibExt/Computability/Complexity/CookLevin/Family.lean:132
def capH (m T d : ℕ) : ℕ := m + (T + 1) * d + 1CSLibExt/Computability/Complexity/CookLevin/Situation.lean:1420
def depth (M : FinTM2) : ℕ :=
letI := M.ΛFin
Finset.univ.sup fun l => ops (M.m l)CSLibExt/Computability/Complexity/CookLevin/Situation.lean:231
def shFamily (N T H : ℕ) : CNF :=
(List.range T).flatMap fun t => (List.range N).flatMap fun i =>
(List.range L.KK).flatMap fun k => shBlk L sa pl cn pu T H t i kCSLibExt/Computability/Complexity/CookLevin/Shift.lean:100
def Accepts (M : FinTM2) (c : M.Cfg) (acc : M.Γ M.k₁) : Prop :=
c.l = none ∧ c.var = M.initialState ∧ (c.stk M.k₁).head? = some accCSLibExt/Computability/Complexity/CookLevin/Situation.lean:2019
def runI (M : FinTM2) (c : M.Cfg) : ℕ → M.Cfg
| 0 => c
| t + 1 => stepI M (runI M c t)CSLibExt/Computability/Complexity/CookLevin/Situation.lean:691
Uses 23 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.