Cell literals propagate one step along the real run to The init family discharges the init obligation

TheoremCell literals propagate one step along the real run#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with window depth \(d\), let \(s\) be a list of symbols of the input stack of \(M\), and for each \(n\) let \(c_n\) be the configuration after \(n\) steps of the idle-extended run of \(M\) from its initial configuration on \(s\). Let \(T, H, t\) be natural numbers with \(t < T\) and \(d \le H\). Suppose an assignment \(a\) satisfies the transition clause family of \(E\) with the situation-variable table \(\mathrm{sa}\) in place of the next-label table (the S-definition family) at \(T\), \(H\) and the number \(N\) of situations of \(E\), and satisfies the cell-shift clause family of \(E\) at \(N\), \(T\), \(H\). Suppose also that every stack of \(c_t\) has length at most \(H - d\), that the code literal of \(c_t\) holds in row \(t\) (the label/state variable of row \(t\) for the code of \(c_t\) is true under \(a\)), and that the cell literals of \(c_t\) hold in row \(t\) (for every stack number \(k\) below the number of stacks and every depth \(j < H\), the cell variable of row \(t\) for stack \(k\), depth \(j\) and the code of the symbol of \(c_t\) there, \(0\) if there is none, is true under \(a\)). Then the cell literals of \(c_{t+1}\) hold in row \(t + 1\).

theorem cells_step_run {T H t : ℕ} {a : List Bool} (s : List (M.Γ M.k₀))
    (hs : cnfSat (Family.family E.layout E.la E.sa E.wa T H E.N) a)
    (ha : cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T H) a) (ht : t < T)
    (hh : ∀ k, ((runI M (initList M s) t).stk k).length ≤ H - depth M) (hdH : depth M ≤ H)
    (hcode : E.CodeHolds a H t (runI M (initList M s) t))
    (hrow : E.CellsHold a H t (E.cell (runI M (initList M s) t))) :
    E.CellsHold a H (t + 1) (E.cell (runI M (initList M s) (t + 1)))

Uses 26 · Used by 1

Statement usesThe transition clause family · The cell-shift clause family · Encoding data for a finite TM2 machine · Cell literals of an array hold in a row · The code of a configuration holds in a row · Number of situations · Cell code of a configuration · Consumption table of a situation · Label/state code of a situation · Clause layout of a machine encoding · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesIndex of a cell variable in the transition-family layout · Index of a label/state variable · Overflow cells of the next row on a real run · Pushed-fill forcing on a real run · L3 (S-definition, real run) · Positive shift step on a real run (L3⁺) · Situation index of a configuration · Truth of a variable under an assignment · The three depth regions cover every depth exactly once

Used byOne-step invariant

TheoremOne-step invariant#✓fully proved

Fix an encoding \(E\) of a machine \(M\) with \(K\) stacks, window depth \(d\) and \(N\) situations, natural numbers \(T\), \(H\), \(t\) with \(t < T\) and \(d \le H\), an assignment \(a\) and an input list \(s\), and let \(c_t\) be the configuration at time \(t\) of the idle-extended run of \(M\) from the start configuration on \(s\). Suppose \(a\) satisfies the transition clause families of the layout of \(E\) with tables \((\mathrm{la}, \mathrm{na}, \mathrm{wa})\) and \((\mathrm{la}, \mathrm{sa}, \mathrm{wa})\) and the cell-shift clause family with tables \((\mathrm{sa}, \mathrm{pl}, \mathrm{cn}, \mathrm{pu})\), all for time bound \(T\), height \(H\) and \(N\) situations. Say that a configuration \(c\) is tracked in row \(t\) when, in the layout of \(E\) at height \(H\), the literal of the (label, state) code of \(c\) in row \(t\) is true under \(a\) and, for every stack number \(k < K\) and depth \(j < H\), the literal of the cell code of \(c\) at stack \(k\) and depth \(j\) in row \(t\) is true under \(a\). If every stack of \(c_t\) has length at most \(H - d\) and \(c_t\) is tracked in row \(t\), then \(c_{t+1}\) is tracked in row \(t + 1\).

theorem row_step_run {T H t : ℕ} {a : List Bool} (s : List (M.Γ M.k₀))
    (hu : cnfSat (Family.family E.layout E.la E.na E.wa T H E.N) a)
    (hs : cnfSat (Family.family E.layout E.la E.sa E.wa T H E.N) a)
    (ha : cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T H) a) (ht : t < T)
    (hh : ∀ k, ((runI M (initList M s) t).stk k).length ≤ H - depth M) (hdH : depth M ≤ H)
    (hcode : E.CodeHolds a H t (runI M (initList M s) t))
    (hrow : E.CellsHold a H t (E.cell (runI M (initList M s) t))) :
    E.CodeHolds a H (t + 1) (runI M (initList M s) (t + 1)) ∧
      E.CellsHold a H (t + 1) (E.cell (runI M (initList M s) (t + 1)))

Uses 20 · Used by 2

Statement usesThe transition clause family · The cell-shift clause family · Encoding data for a finite TM2 machine · Cell literals of an array hold in a row · The code of a configuration holds in a row · Number of situations · Cell code of a configuration · Consumption table of a situation · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesCell literals propagate one step along the real run · Update forcing, real run

Used byOne-step invariant at the stack cap · Row-\(t\) induction

TheoremOne-step invariant at the stack cap#✓fully proved

Fix an encoding \(E\) of a machine \(M\) with \(K\) stacks, window depth \(d\) and \(N\) situations, natural numbers \(m\), \(T\), \(t\) with \(t < T\), an assignment \(a\) and an input list \(s\) of length at most \(m\). Let \(H = m + (T + 1)d + 1\) be the stack cap and let \(c_t\) be the configuration at time \(t\) of the idle-extended run of \(M\) from the start configuration on \(s\). Suppose \(a\) satisfies the transition clause families of the layout of \(E\) with tables \((\mathrm{la}, \mathrm{na}, \mathrm{wa})\) and \((\mathrm{la}, \mathrm{sa}, \mathrm{wa})\) and the cell-shift clause family with tables \((\mathrm{sa}, \mathrm{pl}, \mathrm{cn}, \mathrm{pu})\), all for time bound \(T\), height \(H\) and \(N\) situations. Say that a configuration \(c\) is tracked in row \(t\) when, in the layout of \(E\) at height \(H\), the literal of the (label, state) code of \(c\) in row \(t\) is true under \(a\) and, for every stack number \(k < K\) and depth \(j < H\), the literal of the cell code of \(c\) at stack \(k\) and depth \(j\) in row \(t\) is true under \(a\). If \(c_t\) is tracked in row \(t\), then \(c_{t+1}\) is tracked in row \(t + 1\).

theorem row_step_capH {m T t : ℕ} {a : List Bool} (s : List (M.Γ M.k₀)) (hsm : s.length ≤ m)
    (hu : cnfSat (Family.family E.layout E.la E.na E.wa T (capH m T (depth M)) E.N) a)
    (hs : cnfSat (Family.family E.layout E.la E.sa E.wa T (capH m T (depth M)) E.N) a)
    (ha : cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T (capH m T (depth M))) a)
    (ht : t < T)
    (hcode : E.CodeHolds a (capH m T (depth M)) t (runI M (initList M s) t))
    (hrow : E.CellsHold a (capH m T (depth M)) t (E.cell (runI M (initList M s) t))) :
    E.CodeHolds a (capH m T (depth M)) (t + 1) (runI M (initList M s) (t + 1)) ∧
      E.CellsHold a (capH m T (depth M)) (t + 1) (E.cell (runI M (initList M s) (t + 1)))

Uses 21

Statement usesThe transition clause family · The cell-shift clause family · Encoding data for a finite TM2 machine · Cell literals of an array hold in a row · The code of a configuration holds in a row · Number of situations · Cell code of a configuration · Consumption table of a situation · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation · Stack cap · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesOne-step invariant · Stack heights are at most the cap minus the window depth

DefinitionRow-0 obligation#✓fully proved

For an encoding \(E\) of a machine \(M\) with \(K\) stacks, an assignment \(a\), a height \(H\) and an input list \(s\), let \(c\) be the start configuration of \(M\) on \(s\). The row-0 obligation says that, in the layout of \(E\) at height \(H\), the literal of the (label, state) code of \(c\) in row \(0\) is true under \(a\) and, for every stack number \(k < K\) and depth \(j < H\), the literal of the cell code of \(c\) at stack \(k\) and depth \(j\) in row \(0\) is true under \(a\).

This is a positive form: the literals of the other cell codes are not required to be false.

def Row0 (a : List Bool) (H : ℕ) (s : List (M.Γ M.k₀)) : Prop :=
  E.CodeHolds a H 0 (initList M s) ∧ E.CellsHold a H 0 (E.cell (initList M s))

Uses 4 · Used by 5

Statement usesEncoding data for a finite TM2 machine · Cell literals of an array hold in a row · The code of a configuration holds in a row · Cell code of a configuration

Used byInit obligation, input pinned · Init semantics · Row induction at the stack cap · Run tracking from the init obligation · Row-\(t\) induction

DefinitionInit obligation, input pinned#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with window depth \(d\), let \(a\) be an assignment, let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), and let \(m, T\) be natural numbers, and put \(H = m + (T + 1)d + 1\). The init obligation for \(a\), \(x\), \(Y\), \(m\) and \(T\) holds when there is a list \(y\) of symbols of \(Y\) with \(|x| + |y| \le m\) such that the row-0 obligation holds for \(a\) at height \(H\) and the input \(x\) followed by \(y\): under \(a\), the code literal of row \(0\) and the cell literals of row \(0\) at every depth below \(H\) are true for the initial configuration of \(M\) on that input.

def InitObl (a : List Bool) (x Ys : List (M.Γ M.k₀)) (m T : ℕ) : Prop :=
  ∃ y : List (M.Γ M.k₀), (∀ z ∈ y, z ∈ Ys) ∧ (x ++ y).length ≤ m ∧
    E.Row0 a (capH m T (depth M)) (x ++ y)

Uses 4 · Used by 2

Statement usesEncoding data for a finite TM2 machine · Row-0 obligation · Stack cap · Window depth of a machine

Used byThe init family discharges the init obligation · Run tracking from the init obligation

TheoremRow-\(t\) induction#✓fully proved

Fix an encoding \(E\) of a machine \(M\) with \(K\) stacks, window depth \(d\) and \(N\) situations, natural numbers \(T\) and \(H\) with \(d \le H\), an assignment \(a\) and an input list \(s\), and let \(c_t\) be the configuration at time \(t\) of the idle-extended run of \(M\) from the start configuration on \(s\). Suppose \(a\) satisfies the transition clause families of the layout of \(E\) with tables \((\mathrm{la}, \mathrm{na}, \mathrm{wa})\) and \((\mathrm{la}, \mathrm{sa}, \mathrm{wa})\) and the cell-shift clause family with tables \((\mathrm{sa}, \mathrm{pl}, \mathrm{cn}, \mathrm{pu})\), all for time bound \(T\), height \(H\) and \(N\) situations. Say that a configuration \(c\) is tracked in row \(t\) when, in the layout of \(E\) at height \(H\), the literal of the (label, state) code of \(c\) in row \(t\) is true under \(a\) and, for every stack number \(k < K\) and depth \(j < H\), the literal of the cell code of \(c\) at stack \(k\) and depth \(j\) in row \(t\) is true under \(a\). If, for every \(t < T\), every stack of \(c_t\) has length at most \(H - d\), and the row-0 obligation holds for \(a\), height \(H\) and the input \(s\), then \(c_t\) is tracked in row \(t\) for every \(t \le T\).

theorem rows_run {T H : ℕ} {a : List Bool} (s : List (M.Γ M.k₀))
    (hu : cnfSat (Family.family E.layout E.la E.na E.wa T H E.N) a)
    (hs : cnfSat (Family.family E.layout E.la E.sa E.wa T H E.N) a)
    (ha : cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T H) a)
    (hh : ∀ t < T, ∀ k, ((runI M (initList M s) t).stk k).length ≤ H - depth M)
    (hdH : depth M ≤ H) (h0 : E.Row0 a H s) :
    ∀ t ≤ T, E.CodeHolds a H t (runI M (initList M s) t) ∧
      E.CellsHold a H t (E.cell (runI M (initList M s) t))

Uses 20 · Used by 1

Statement usesThe transition clause family · The cell-shift clause family · Encoding data for a finite TM2 machine · Cell literals of an array hold in a row · The code of a configuration holds in a row · Number of situations · Row-0 obligation · Cell code of a configuration · Consumption table of a situation · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesOne-step invariant

Used byRow induction at the stack cap

TheoremRow induction at the stack cap#✓fully proved

Fix an encoding \(E\) of a machine \(M\) with \(K\) stacks, window depth \(d\) and \(N\) situations, natural numbers \(m\) and \(T\), an assignment \(a\) and an input list \(s\) of length at most \(m\). Let \(H = m + (T + 1)d + 1\) be the stack cap and let \(c_t\) be the configuration at time \(t\) of the idle-extended run of \(M\) from the start configuration on \(s\). Suppose \(a\) satisfies the transition clause families of the layout of \(E\) with tables \((\mathrm{la}, \mathrm{na}, \mathrm{wa})\) and \((\mathrm{la}, \mathrm{sa}, \mathrm{wa})\) and the cell-shift clause family with tables \((\mathrm{sa}, \mathrm{pl}, \mathrm{cn}, \mathrm{pu})\), all for time bound \(T\), height \(H\) and \(N\) situations. Say that a configuration \(c\) is tracked in row \(t\) when, in the layout of \(E\) at height \(H\), the literal of the (label, state) code of \(c\) in row \(t\) is true under \(a\) and, for every stack number \(k < K\) and depth \(j < H\), the literal of the cell code of \(c\) at stack \(k\) and depth \(j\) in row \(t\) is true under \(a\). If the row-0 obligation holds for \(a\), height \(H\) and the input \(s\), then \(c_t\) is tracked in row \(t\) for every \(t \le T\).

theorem rows_capH {m T : ℕ} {a : List Bool} (s : List (M.Γ M.k₀)) (hsm : s.length ≤ m)
    (hu : cnfSat (Family.family E.layout E.la E.na E.wa T (capH m T (depth M)) E.N) a)
    (hs : cnfSat (Family.family E.layout E.la E.sa E.wa T (capH m T (depth M)) E.N) a)
    (ha : cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T (capH m T (depth M))) a)
    (h0 : E.Row0 a (capH m T (depth M)) s) :
    ∀ t ≤ T, E.CodeHolds a (capH m T (depth M)) t (runI M (initList M s) t) ∧
      E.CellsHold a (capH m T (depth M)) t (E.cell (runI M (initList M s) t))

Uses 22 · Used by 1

Statement usesThe transition clause family · The cell-shift clause family · Encoding data for a finite TM2 machine · Cell literals of an array hold in a row · The code of a configuration holds in a row · Number of situations · Row-0 obligation · Cell code of a configuration · Consumption table of a situation · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation · Stack cap · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesRow-\(t\) induction · Stack heights are at most the cap minus the window depth

Used byRun tracking from the init obligation

TheoremRun tracking from the init obligation#✓fully proved

Fix an encoding \(E\) of a machine \(M\) with \(K\) stacks, window depth \(d\) and \(N\) situations, lists \(x\) and \(Y\) of input symbols, natural numbers \(m\) and \(T\), and an assignment \(a\), and let \(H = m + (T + 1)d + 1\) be the stack cap. Suppose \(a\) satisfies the transition clause families of the layout of \(E\) with tables \((\mathrm{la}, \mathrm{na}, \mathrm{wa})\) and \((\mathrm{la}, \mathrm{sa}, \mathrm{wa})\) and the cell-shift clause family with tables \((\mathrm{sa}, \mathrm{pl}, \mathrm{cn}, \mathrm{pu})\), all for time bound \(T\), height \(H\) and \(N\) situations. Say that a configuration \(c\) is tracked in row \(t\) when, in the layout of \(E\) at height \(H\), the literal of the (label, state) code of \(c\) in row \(t\) is true under \(a\) and, for every stack number \(k < K\) and depth \(j < H\), the literal of the cell code of \(c\) at stack \(k\) and depth \(j\) in row \(t\) is true under \(a\). If the init obligation holds for \(a\), \(x\), \(Y\), \(m\) and \(T\), then there is a list \(y\) of input symbols, each occurring in \(Y\), such that the concatenation \(xy\) has length at most \(m\) and, for every \(t \le T\), the configuration at time \(t\) of the idle-extended run of \(M\) from the start configuration on \(xy\) is tracked in row \(t\).

theorem rows_of_init {x Ys : List (M.Γ M.k₀)} {m T : ℕ} {a : List Bool}
    (hu : cnfSat (Family.family E.layout E.la E.na E.wa T (capH m T (depth M)) E.N) a)
    (hs : cnfSat (Family.family E.layout E.la E.sa E.wa T (capH m T (depth M)) E.N) a)
    (ha : cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T (capH m T (depth M))) a)
    (hI : E.InitObl a x Ys m T) :
    ∃ y : List (M.Γ M.k₀), (∀ z ∈ y, z ∈ Ys) ∧ (x ++ y).length ≤ m ∧
      ∀ t ≤ T, E.CodeHolds a (capH m T (depth M)) t (runI M (initList M (x ++ y)) t) ∧
        E.CellsHold a (capH m T (depth M)) t (E.cell (runI M (initList M (x ++ y)) t))

Uses 22 · Used by 1

Statement usesThe transition clause family · The cell-shift clause family · Encoding data for a finite TM2 machine · Cell literals of an array hold in a row · The code of a configuration holds in a row · Init obligation, input pinned · Number of situations · Cell code of a configuration · Consumption table of a situation · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation · Stack cap · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesRow-0 obligation · Row induction at the stack cap

Used byA satisfying assignment tracks a certified run

TheoremSatisfying a concatenation of CNF formulas#✓fully proved

For dense CNF formulas \(\varphi\) and \(\psi\) and a finite bit sequence \(a\), \(a\) satisfies the concatenation of \(\varphi\) and \(\psi\) (the clauses of \(\varphi\) followed by those of \(\psi\)) if and only if \(a\) satisfies both \(\varphi\) and \(\psi\).

theorem cnfSat_append {φ ψ : CNF} {a : List Bool} : cnfSat (φ ++ ψ) a ↔ cnfSat φ a ∧ cnfSat ψ a

Uses 4 · Used by 3

Statement usesDense CNF formula · Dense clause · Satisfaction of a dense CNF formula

Proof usesSatisfaction of a dense clause

Used byInit semantics · Completeness of the init family · Correctness of the assembled formula

TheoremPositive dense unit clauses force their variable#✓fully proved

If an assignment \(a\) satisfies a CNF formula \(\varphi\) containing the dense clause over \(V\) variables built from the literal list whose only entry is the pair \((v, \mathrm{true})\), then variable \(v\) is true under \(a\).

theorem unit_force {V v : ℕ} {φ : CNF} {a : List Bool} (h : cnfSat φ a)
    (hm : Family.denseClause V [(v, true)] ∈ φ) : Tr a v

Uses 6 · Used by 1

Statement usesDense clause from a list of literals · Truth of a variable under an assignment · Dense CNF formula · Dense clause · Satisfaction of a dense CNF formula

Proof usesL0 (a satisfied dense clause has a satisfied listed literal)

Used byInit semantics

DefinitionIndex of the empty-cell variable of the input stack#✓fully proved

For an encoding \(E\) and natural numbers \(H\) and \(j\), this is the index, in the layout of \(E\) at height \(H\), of the cell variable for row \(0\), the stack number of the input stack, depth \(j\) from the top and symbol code \(0\) (the empty cell).

def zIdx (H j : ℕ) : ℕ := E.layout.cIdx H 0 (E.kc M.k₀) j 0

Uses 3 · Used by 8

Statement usesIndex of a cell variable in the transition-family layout · Encoding data for a finite TM2 machine · Clause layout of a machine encoding

Used byThe init family of an encoding is a layout-level init family · Certificate clauses of the init family · Prefix clauses of the init family · Init semantics · Length-bound clauses of the init family · The init family is faithful with positive literals · Completeness of the init family · Every clause of the Cook–Levin formula has one slot per variable

DefinitionStart-code clause of the init family#✓fully proved

Let \(E\) be an encoding of a machine \(M\) and let \(T, H\) be natural numbers. The start-code clause is the CNF formula with a single clause: the dense clause over the \((T + 1)W\) variables of the layout of \(E\), where \(W\) is its row width at height \(H\), whose only literal is the positive literal of the label/state variable of row \(0\) for the code under \(E\) of the pair formed by the main label of \(M\) and its initial state.

def initCode (T H : ℕ) : CNF :=
  [Family.denseClause (E.layout.numVars T H) [(E.layout.xIdx H 0 (E.lc (some M.main,
      M.initialState)), true)]]

Uses 7 · Used by 6

Statement usesNumber of variables of the transition-clause formula · Index of a label/state variable · Dense clause from a list of literals · Encoding data for a finite TM2 machine · Clause layout of a machine encoding · Dense CNF formula · Dense clause

Used byThe init family of an encoding is a layout-level init family · The row-0 init family of an encoding · Init semantics · The init family is faithful with positive literals · Completeness of the init family · Every clause of the Cook–Levin formula has one slot per variable

DefinitionEmpty-stack clauses of the init family#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with \(K\) numbered stacks and let \(T, H\) be natural numbers. The empty-stack clauses form the CNF formula that lists, for each stack number \(k < K\) other than the number of the input stack in increasing order and, within it, each depth \(j < H\) in increasing order, the dense clause over the \((T + 1)W\) variables of the layout of \(E\), where \(W\) is its row width at height \(H\), whose only literal is the positive literal of the cell variable of row \(0\) for stack \(k\), depth \(j\) and code \(0\), the empty cell. They ask that every stack other than the input stack be empty in row \(0\).

def initOther (T H : ℕ) : CNF :=
  ((List.range E.KK).filter (· ≠ E.kc M.k₀)).flatMap fun k =>
    (List.range H).map fun j => Family.denseClause (E.layout.numVars T H) [(E.layout.cIdx H 0 k j 0, true)]

Uses 7 · Used by 6

Statement usesIndex of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Dense clause from a list of literals · Encoding data for a finite TM2 machine · Clause layout of a machine encoding · Dense CNF formula · Dense clause

Used byThe init family of an encoding is a layout-level init family · The row-0 init family of an encoding · Init semantics · The init family is faithful with positive literals · Completeness of the init family · Every clause of the Cook–Levin formula has one slot per variable

DefinitionInput clauses of the init family#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(x = x_0 x_1 \cdots x_{n-1}\) be a list of symbols of the input stack of \(M\), and let \(T, H\) be natural numbers. The input clauses form the CNF formula that lists, for \(j = 0, 1, \dots, n - 1\) in order, the dense clause over the \((T + 1)W\) variables of the layout of \(E\), where \(W\) is its row width at height \(H\), whose only literal is the positive literal of the cell variable of row \(0\) for the input stack, depth \(j\) and the symbol code under \(E\) of \(x_j\). They pin the input \(x\) at the top of the input stack, one cell at a time.

def initIn (x : List (M.Γ M.k₀)) (T H : ℕ) : CNF :=
  (List.range x.length).map fun j => Family.denseClause (E.layout.numVars T H)
    [(E.layout.cIdx H 0 (E.kc M.k₀) j ((x[j]?).elim 0 (E.enc M.k₀)), true)]

Uses 7 · Used by 6

Statement usesIndex of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Dense clause from a list of literals · Encoding data for a finite TM2 machine · Clause layout of a machine encoding · Dense CNF formula · Dense clause

Used byThe init family of an encoding is a layout-level init family · The row-0 init family of an encoding · Init semantics · The init family is faithful with positive literals · Completeness of the init family · Every clause of the Cook–Levin formula has one slot per variable

DefinitionCertificate clauses of the init family#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), and let \(m, T, H\) be natural numbers. For a depth \(j\) and a symbol code \(c\), write \(C_0[j, c]\) for the cell variable of row \(0\), input stack, depth \(j\) and code \(c\) in the layout of \(E\) at height \(H\), and let \(e\) be the symbol code of \(E\) on the input stack. The certificate clauses form the CNF formula that lists, for each depth \(j = |x|, |x| + 1, \dots, m - 1\) in order (none if \(m \le |x|\)), the dense clause over the \((T + 1)W\) variables of the layout, where \(W\) is its row width at height \(H\), whose literals are \(C_0[j, 0]\) followed by \(C_0[j, e(z)]\) for each \(z\) in \(Y\) in order, all positive.

Code \(0\) is the empty cell, so the clause for \(j\) asks that depth \(j\) of the input stack be empty or hold a symbol of \(Y\).

def initCert (x Ys : List (M.Γ M.k₀)) (m T H : ℕ) : CNF :=
  (List.range (m - x.length)).map fun i => Family.denseClause (E.layout.numVars T H)
    ((E.zIdx H (x.length + i), true) ::
      Ys.map fun z => (E.layout.cIdx H 0 (E.kc M.k₀) (x.length + i) (E.enc M.k₀ z), true))

Uses 8 · Used by 6

Statement usesIndex of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Dense clause from a list of literals · Encoding data for a finite TM2 machine · Clause layout of a machine encoding · Index of the empty-cell variable of the input stack · Dense CNF formula · Dense clause

Used byThe init family of an encoding is a layout-level init family · The row-0 init family of an encoding · Init semantics · The init family is faithful with positive literals · Completeness of the init family · Every clause of the Cook–Levin formula has one slot per variable

DefinitionPrefix clauses of the init family#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(x\) be a list of symbols of the input stack of \(M\), and let \(m, T, H\) be natural numbers. For a depth \(j\), write \(Z_j\) for the cell variable of row \(0\), input stack, depth \(j\) and code \(0\) (the empty cell) in the layout of \(E\) at height \(H\). The prefix clauses form the CNF formula that lists, for \(j = |x|, |x| + 1, \dots, m - 1\) in order (none if \(m \le |x|\)), the dense clause over the \((T + 1)W\) variables of the layout, where \(W\) is its row width at height \(H\), with the literals \(\neg Z_j\) and \(Z_{j+1}\). On these depths, an empty cell forces an empty cell one level deeper.

def initPre (x : List (M.Γ M.k₀)) (m T H : ℕ) : CNF :=
  (List.range (m - x.length)).map fun i => Family.denseClause (E.layout.numVars T H)
    [(E.zIdx H (x.length + i), false), (E.zIdx H (x.length + i + 1), true)]

Uses 7 · Used by 6

Statement usesNumber of variables of the transition-clause formula · Dense clause from a list of literals · Encoding data for a finite TM2 machine · Clause layout of a machine encoding · Index of the empty-cell variable of the input stack · Dense CNF formula · Dense clause

Used byThe init family of an encoding is a layout-level init family · The row-0 init family of an encoding · Init semantics · The init family is faithful with positive literals · Completeness of the init family · Every clause of the Cook–Levin formula has one slot per variable

DefinitionLength-bound clauses of the init family#✓fully proved

For an encoding \(E\) and natural numbers \(m\), \(T\) and \(H\), this is the CNF formula with one clause for each depth \(j\) with \(m \le j < H\), in increasing order of \(j\): the dense clause over the variables of the transition-clause formula of the layout of \(E\) at bounds \(T\) and \(H\), built from the single positive literal of the empty-cell variable of the input stack at depth \(j\) in row \(0\).

def initTail (m T H : ℕ) : CNF :=
  (List.range (H - m)).map fun i => Family.denseClause (E.layout.numVars T H) [(E.zIdx H (m + i),
      true)]

Uses 7 · Used by 5

Statement usesNumber of variables of the transition-clause formula · Dense clause from a list of literals · Encoding data for a finite TM2 machine · Clause layout of a machine encoding · Index of the empty-cell variable of the input stack · Dense CNF formula · Dense clause

Used byThe init family of an encoding is a layout-level init family · The row-0 init family of an encoding · Init semantics · The init family is faithful with positive literals · Completeness of the init family

DefinitionThe row-0 init family of an encoding#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), and let \(m, T, H\) be natural numbers. The init family is the CNF formula whose clauses are, in this order, those of the start-code clause at \((T, H)\), the empty-stack clauses at \((T, H)\), the input clauses of \(x\) at \((T, H)\), the certificate clauses of \(x\) and \(Y\) at \((m, T, H)\), the prefix clauses of \(x\) at \((m, T, H)\) and the tail clauses at \((m, T, H)\).

Together they ask that row \(0\) hold the start code, empty stacks other than the input stack, the input \(x\) at the top of the input stack, cells that are empty or hold a symbol of \(Y\) at the depths \(|x| \le j < m\), with an empty cell at such a depth \(j\) forcing an empty cell at \(j + 1\), and empty cells at the depths \(m \le j < H\).

def initFamily (x Ys : List (M.Γ M.k₀)) (m T H : ℕ) : CNF :=
  E.initCode T H ++ E.initOther T H ++ E.initIn x T H ++ E.initCert x Ys m T H ++
    E.initPre x m T H ++ E.initTail m T H

Uses 9 · Used by 17

Statement usesEncoding data for a finite TM2 machine · Certificate clauses of the init family · Start-code clause of the init family · Input clauses of the init family · Empty-stack clauses of the init family · Prefix clauses of the init family · Length-bound clauses of the init family · Dense CNF formula · Dense clause

Used byThe init family of an encoding is a layout-level init family · The init generator at the stack cap · Time and output of the init generator for an encoding · The init family discharges the init obligation · Init semantics · Satisfying assignments yield accepting runs · The init family is faithful with positive literals · A satisfying assignment tracks a certified run · The all-true assignment satisfies the transition, shift and init families · No accepting certificate, no satisfying assignment · Completeness of the five clause families · Completeness of the init family · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · The assembled generator, after the precomputation · Every clause of the Cook–Levin formula has one slot per variable

TheoremInit semantics#✓fully proved

Fix an encoding \(E\) of a machine \(M\), lists \(x\) and \(Y\) of symbols of the input alphabet, natural numbers \(m\), \(T\), \(H\) with \(|x| \le m < H\), and an assignment \(a\) that satisfies the init family of \(E\) for \(x\), \(Y\), \(m\), \(T\) and \(H\). Then there is a list \(y\) of input symbols, each occurring in \(Y\), such that the concatenation \(xy\) has length at most \(m\) and the row-0 obligation holds for \(a\), height \(H\) and the input \(xy\).

theorem init_row0 {x Ys : List (M.Γ M.k₀)} {m T H : ℕ} {a : List Bool}
    (hx : x.length ≤ m) (hmH : m < H) (hI : cnfSat (E.initFamily x Ys m T H) a) :
    ∃ y : List (M.Γ M.k₀), (∀ z ∈ y, z ∈ Ys) ∧ (x ++ y).length ≤ m ∧ E.Row0 a H (x ++ y)

Uses 26 · Used by 1

Statement usesEncoding data for a finite TM2 machine · Row-0 obligation · The row-0 init family of an encoding · Satisfaction of a dense CNF formula

Proof usesIndex of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Index of a label/state variable · Dense clause from a list of literals · Cell literals of an array hold in a row · The code of a configuration holds in a row · Cell code of a configuration · Label-and-state code of a configuration · Certificate clauses of the init family · Start-code clause of the init family · Input clauses of the init family · Empty-stack clauses of the init family · Prefix clauses of the init family · Length-bound clauses of the init family · Clause layout of a machine encoding · Index of the empty-cell variable of the input stack · Truth of a variable under an assignment · L0 (a satisfied dense clause has a satisfied listed literal) · Satisfying a concatenation of CNF formulas · Positive dense unit clauses force their variable · Dense CNF formula · Dense clause

Used byThe init family discharges the init obligation

TheoremThe init family discharges the init obligation#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with window depth \(d\), let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), and let \(m, T\) be natural numbers with \(|x| \le m\), and put \(H = m + (T + 1)d + 1\). If an assignment \(a\) satisfies the init family of \(E\) for \(x\), \(Y\), \(m\), \(T\) and \(H\), then the init obligation holds for \(a\), \(x\), \(Y\), \(m\) and \(T\): there is a list \(y\) of symbols of \(Y\) with \(|x| + |y| \le m\) such that the row-0 obligation holds for \(a\) at height \(H\) and the input \(x\) followed by \(y\).

theorem init_obl {x Ys : List (M.Γ M.k₀)} {m T : ℕ} {a : List Bool} (hx : x.length ≤ m)
    (hI : cnfSat (E.initFamily x Ys m T (capH m T (depth M))) a) : E.InitObl a x Ys m T

Uses 7 · Used by 1

Statement usesEncoding data for a finite TM2 machine · Init obligation, input pinned · The row-0 init family of an encoding · Stack cap · Window depth of a machine · Satisfaction of a dense CNF formula

Proof usesInit semantics

Used byA satisfying assignment tracks a certified run

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.