Transition clauses force the next label to The three depth regions cover every depth exactly once

TheoremTransition clauses force the next label#✓fully proved

Let \(L\) be a layout with \(K\) stacks and window depth \(d\), let \(\mathrm{la}, \mathrm{na} : \mathbb{N} \to \mathbb{N}\) and \(\mathrm{wa} : \mathbb{N} \to \mathbb{N} \to \mathbb{N} \to \mathbb{N}\) be tables, and let \(a\) be an assignment satisfying the transition clause family of \(L\), \(\mathrm{la}\), \(\mathrm{na}\) and \(\mathrm{wa}\) for bounds \(T\), \(H\) and \(N\). Write \(X[t, b]\) and \(C[t, k, j, x]\) for the label/state and cell variables at height \(H\). Suppose \(t < T\), \(i < N\), \(X[t, \mathrm{la}(i)]\) is true under \(a\), and for every \(n < Kd\), writing \(q = \lfloor n / d \rfloor\) and \(r = n \bmod d\), the variable \(C[t, q, r, \mathrm{wa}(i, q, r)]\) is true under \(a\). Then \(X[t + 1, \mathrm{na}(i)]\) is true under \(a\).

The window literals are indexed by \(n\) exactly as in the clause, and no one-hot hypothesis on \(a\) is needed.

theorem fam_force {L : Family.Layout} {la na : ℕ → ℕ} {wa : ℕ → ℕ → ℕ → ℕ} {N T H : ℕ}
    {a : List Bool} (ha : cnfSat (Family.family L la na wa T H N) a) {t i : ℕ} (ht : t < T)
    (hi : i < N) (hX : Tr a (L.xIdx H t (la i)))
    (hW : ∀ n < L.KK * L.d, Tr a (L.cIdx H t (n / L.d) (n % L.d) (wa i (n / L.d) (n % L.d)))) :
    Tr a (L.xIdx H (t + 1) (na i))

Uses 14 · Used by 1

Statement usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Index of a label/state variable · The transition clause family · Truth of a variable under an assignment · Satisfaction of a dense CNF formula

Proof usesNumber of literals of a transition clause · Number of variables of the transition-clause formula · Dense clause from a list of literals · Position of a literal in a transition clause · Literals of a transition clause · L0 (a satisfied dense clause has a satisfied listed literal) · Dense CNF formula · Dense clause

Used byTransition clauses force the next label, stack-and-depth form

TheoremTransition clauses force the next label, stack-and-depth form#✓fully proved

Let \(L\) be a layout with \(K\) stacks and window depth \(d\), let \(\mathrm{la}, \mathrm{na} : \mathbb{N} \to \mathbb{N}\) and \(\mathrm{wa} : \mathbb{N} \to \mathbb{N} \to \mathbb{N} \to \mathbb{N}\) be tables, and let \(a\) be an assignment satisfying the transition clause family of \(L\), \(\mathrm{la}\), \(\mathrm{na}\) and \(\mathrm{wa}\) for bounds \(T\), \(H\) and \(N\). Write \(X[t, b]\) and \(C[t, k, j, x]\) for the label/state and cell variables at height \(H\). If \(t < T\), \(i < N\), \(X[t, \mathrm{la}(i)]\) is true under \(a\), and \(C[t, k, j, \mathrm{wa}(i, k, j)]\) is true under \(a\) for all \(k < K\) and \(j < d\), then \(X[t + 1, \mathrm{na}(i)]\) is true under \(a\).

theorem fam_force_kj {L : Family.Layout} {la na : ℕ → ℕ} {wa : ℕ → ℕ → ℕ → ℕ} {N T H : ℕ}
    {a : List Bool} (ha : cnfSat (Family.family L la na wa T H N) a) {t i : ℕ} (ht : t < T)
    (hi : i < N) (hX : Tr a (L.xIdx H t (la i)))
    (hW : ∀ k < L.KK, ∀ j < L.d, Tr a (L.cIdx H t k j (wa i k j))) :
    Tr a (L.xIdx H (t + 1) (na i))

Uses 7 · Used by 2

Statement usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Index of a label/state variable · The transition clause family · Truth of a variable under an assignment · Satisfaction of a dense CNF formula

Proof usesTransition clauses force the next label

Used byL2 (S-definition, positive) · Update forcing (positive)

DefinitionThe code of a configuration holds in a row#✓fully proved

Given an encoding of a machine \(M\), an assignment \(a\), a height \(H\), a time \(t\) and a configuration \(c\) of \(M\), the code of \(c\) holds in row \(t\) when the label/state variable of row \(t\) (at height \(H\)) whose index is the combined (label, state) code of \(c\) is true under \(a\).

def CodeHolds (a : List Bool) (H t : ℕ) (c : M.Cfg) : Prop :=
  Tr a (E.layout.xIdx H t (E.code c))

Uses 5 · Used by 15

Statement usesIndex of a label/state variable · Encoding data for a finite TM2 machine · Label-and-state code of a configuration · Clause layout of a machine encoding · Truth of a variable under an assignment

Used byL2 (S-definition, positive) · L3 (S-definition, real run) · Composition with the shift family · Update forcing (positive) · Update forcing, real run · Cell literals propagate one step along the real run · Init semantics · One-step invariant at the stack cap · One-step invariant · Row-0 obligation · Row induction at the stack cap · Run tracking from the init obligation · Row-\(t\) induction · Satisfying assignments yield accepting runs · A satisfying assignment tracks a certified run

TheoremL2 (S-definition, positive)#✓fully proved

Let \(E\) be an encoding of the machine \(M\) with \(K\) stacks and layout \(L\), let \(d\) be the window depth of \(M\), let \(H \in \mathbb{N}\) with \(d \le H\), let \(W\) be the row width of \(L\) at height \(H\), and write \(X[t, x] = tW + x\) for the label/state variables and \(C[t, k, j, x]\) for the cell variable of row \(t\), stack \(k\), depth \(j\) and symbol code \(x\). For a configuration \(c\) write \(\kappa(c)\) for its (label, state) code and \(\gamma_c(k, j)\) for the code of its cell at stack \(k\) and depth \(j\). Let \(T, t \in \mathbb{N}\) with \(t < T\), and let the assignment \(a\) satisfy the transition clause family of \(L\) for \(T\), \(H\) and the number \(N\) of situations, with the current-label table \(\mathrm{la}\) and the window table \(\mathrm{wa}\) of \(E\), and with the table \(\mathrm{sa}\) of \(E\) (where \(\mathrm{sa}(i)\) is the position of the variable of situation \(i\) in the label/state block) in place of the next-label table. Let \(c\) be a good configuration with situation index \(i\) such that \(X[t, \kappa(c)]\) is true under \(a\) and \(C[t, k, j, \gamma_c(k, j)]\) is true under \(a\) for all \(k < K\) and \(j < H\). Then the variable \(X[t + 1, \mathrm{sa}(i)]\) is true under \(a\).

theorem sd_hold {T H t : ℕ} {a : List Bool}
    (ha : cnfSat (Family.family E.layout E.la E.sa E.wa T H E.N) a) (ht : t < T)
    (c : M.Cfg) (hc : E.Good c) (hdH : depth M ≤ H)
    (hcode : E.CodeHolds a H t c) (hrow : E.CellsHold a H t (E.cell c)) :
    Tr a (E.layout.xIdx H (t + 1) (E.sa (E.sitIdx c)))

Uses 21 · Used by 1

Statement usesIndex of a label/state variable · The transition 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 · Good configurations · Number of situations · Cell code of a configuration · Label/state code of a situation · Clause layout of a machine encoding · Position of a situation's variable · Situation index of a configuration · Window symbol code of a situation · Truth of a variable under an assignment · Window depth of a machine · Satisfaction of a dense CNF formula

Proof usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Label-and-state code of a configuration · The situation index matches the code and windows · Transition clauses force the next label, stack-and-depth form

Used byL3 (S-definition, real run)

TheoremL3 (S-definition, real run)#✓fully proved

Let \(E\) be an encoding of the machine \(M\) with \(K\) stacks and layout \(L\), let \(d\) be the window depth of \(M\), let \(H \in \mathbb{N}\) with \(d \le H\), let \(W\) be the row width of \(L\) at height \(H\), and write \(X[t, x] = tW + x\) for the label/state variables and \(C[t, k, j, x]\) for the cell variable of row \(t\), stack \(k\), depth \(j\) and symbol code \(x\). For a configuration \(c\) write \(\kappa(c)\) for its (label, state) code and \(\gamma_c(k, j)\) for the code of its cell at stack \(k\) and depth \(j\). Fix an input list \(s\), let \(c_n\) be the configuration after \(n\) steps of the idle-extended run of \(M\) from the initial configuration on \(s\), let \(T, t \in \mathbb{N}\) with \(t < T\), and let \(i\) be the situation index of \(c_t\). Let the assignment \(a\) satisfy the transition clause family of \(L\) for \(T\), \(H\) and the number \(N\) of situations, with the current-label table \(\mathrm{la}\) and the window table \(\mathrm{wa}\) of \(E\), and with the table \(\mathrm{sa}\) of \(E\) (where \(\mathrm{sa}(i)\) is the position of the variable of situation \(i\) in the label/state block) in place of the next-label table. If \(X[t, \kappa(c_t)]\) is true under \(a\) and \(C[t, k, j, \gamma_{c_t}(k, j)]\) is true under \(a\) for all \(k < K\) and \(j < H\), then the variable \(X[t + 1, \mathrm{sa}(i)]\) is true under \(a\).

theorem sd_step_run {T H t : ℕ} {a : List Bool} (s : List (M.Γ M.k₀))
    (ha : cnfSat (Family.family E.layout E.la E.sa E.wa T H E.N) a) (ht : t < T)
    (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))) :
    Tr a (E.layout.xIdx H (t + 1) (E.sa (E.sitIdx (runI M (initList M s) t))))

Uses 19 · Used by 2

Statement usesIndex of a label/state variable · The transition 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 · Label/state code of a situation · Clause layout of a machine encoding · Position of a situation's variable · Situation index of a configuration · Window symbol code of a situation · Truth of a variable under an assignment · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesGood configurations · The idle-extended step preserves good configurations · L2 (S-definition, positive)

Used byComposition with the shift family · Cell literals propagate one step along the real run

TheoremComposition with the shift family#✓fully proved

Let \(E\) be an encoding of the machine \(M\) with \(K\) stacks, layout \(L\), \(N\) situations and situation tables \(\mathrm{la}\), \(\mathrm{wa}\), \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\) and \(\mathrm{pu}\), let \(d\) be the window depth of \(M\), let \(H \in \mathbb{N}\) with \(d \le H\), and let \(T, t \in \mathbb{N}\) with \(t < T\). Call a variable true under an assignment \(a\) when its index is less than the length of \(a\) and \(a\) is true there. Write \(X[r, x]\) for the label/state variable \(x\) of row \(r\) and \(C[r, k, j, x]\) for the cell variable of row \(r\), stack \(k\), depth \(j\) and symbol code \(x\) (both at height \(H\)). For a configuration \(c\) write \(\kappa(c)\) for its (label, state) code and \(\gamma_c(k, j)\) for the code of its cell at stack \(k\) and depth \(j\) (\(0\) if there is none). Fix an input list \(s\), let \(c_n\) be the configuration after \(n\) steps of the idle-extended run of \(M\) from the initial configuration on \(s\), and let \(i\) be the situation index of \(c_t\). Let \(a\) satisfy both the transition clause family of \(L\) for \(T\), \(H\) and \(N\) with the tables \(\mathrm{la}\) and \(\mathrm{wa}\) and with \(\mathrm{sa}\) in place of the next-label table, and the cell-shift clause family of \(L\) with the tables \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\) for \(N\), \(T\) and \(H\). Suppose that every stack of \(c_t\) has length at most \(H - d\), that \(X[t, \kappa(c_t)]\) is true, and that \(C[t, k', j', \gamma_{c_t}(k', j')]\) is true for all \(k' < K\) and \(j' < H\). Then for every \(k < K\) and every \(j\) with \(\mathrm{pl}(i, k) \le j < H - \max(\mathrm{pl}(i, k), \mathrm{cn}(i, k)) + \mathrm{pl}(i, k)\), the variable \(C[t + 1, k, j, \gamma_{c_{t+1}}(k, j)]\) is true. Subtraction is truncated at \(0\).

theorem sdsh_step_run_pos {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)))
    {k j : ℕ} (hk : k < E.KK) (hj1 : E.pl (E.sitIdx (runI M (initList M s) t)) k ≤ j)
    (hj2 : j < H - max (E.pl (E.sitIdx (runI M (initList M s) t)) k)
      (E.cn (E.sitIdx (runI M (initList M s) t)) k) + E.pl (E.sitIdx (runI M (initList M s) t)) k) :
    Tr a (E.layout.cIdx H (t + 1) k j (E.cell (runI M (initList M s) (t + 1)) k j))

Uses 22

Statement usesIndex of a cell variable in the transition-family layout · The 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 · Situation index of a configuration · Window symbol code of a situation · Truth of a variable under an assignment · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesL3 (S-definition, real run) · Positive shift step on a real run (L3⁺)

TheoremUpdate forcing (positive)#✓fully proved

Let \(E\) be an encoding of the machine \(M\) with \(K\) stacks and layout \(L\), let \(d\) be the window depth of \(M\), let \(H \in \mathbb{N}\) with \(d \le H\), let \(W\) be the row width of \(L\) at height \(H\), and write \(X[t, x] = tW + x\) for the label/state variables and \(C[t, k, j, x]\) for the cell variable of row \(t\), stack \(k\), depth \(j\) and symbol code \(x\). For a configuration \(c\) write \(\kappa(c)\) for its (label, state) code and \(\gamma_c(k, j)\) for the code of its cell at stack \(k\) and depth \(j\). Let \(T, t \in \mathbb{N}\) with \(t < T\), and let the assignment \(a\) satisfy the transition clause family of \(L\) with the current-label table \(\mathrm{la}\), the next-label table \(\mathrm{na}\) and the window table \(\mathrm{wa}\) of \(E\), for \(T\), \(H\) and the number \(N\) of situations. Let \(c\) be a good configuration with situation index \(i\) such that \(X[t, \kappa(c)]\) is true under \(a\) and \(C[t, k, j, \gamma_c(k, j)]\) is true under \(a\) for all \(k < K\) and \(j < H\). Then the variable \(X[t + 1, \mathrm{na}(i)]\) is true under \(a\).

theorem upd_hold {T H t : ℕ} {a : List Bool}
    (ha : cnfSat (Family.family E.layout E.la E.na E.wa T H E.N) a) (ht : t < T)
    (c : M.Cfg) (hc : E.Good c) (hdH : depth M ≤ H)
    (hcode : E.CodeHolds a H t c) (hrow : E.CellsHold a H t (E.cell c)) :
    Tr a (E.layout.xIdx H (t + 1) (E.na (E.sitIdx c)))

Uses 21 · Used by 1

Statement usesIndex of a label/state variable · The transition 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 · Good configurations · Number of situations · Cell code of a configuration · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Situation index of a configuration · Window symbol code of a situation · Truth of a variable under an assignment · Window depth of a machine · Satisfaction of a dense CNF formula

Proof usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Label-and-state code of a configuration · The situation index matches the code and windows · Transition clauses force the next label, stack-and-depth form

Used byUpdate forcing, real run

TheoremUpdate forcing, real run#✓fully proved

Let \(E\) be an encoding of the machine \(M\) with \(K\) stacks and layout \(L\), let \(d\) be the window depth of \(M\), let \(H \in \mathbb{N}\) with \(d \le H\), let \(W\) be the row width of \(L\) at height \(H\), and write \(X[t, x] = tW + x\) for the label/state variables and \(C[t, k, j, x]\) for the cell variable of row \(t\), stack \(k\), depth \(j\) and symbol code \(x\). For a configuration \(c\) write \(\kappa(c)\) for its (label, state) code and \(\gamma_c(k, j)\) for the code of its cell at stack \(k\) and depth \(j\). Fix an input list \(s\), let \(c_n\) be the configuration after \(n\) steps of the idle-extended run of \(M\) from the initial configuration on \(s\), let \(T, t \in \mathbb{N}\) with \(t < T\), and suppose every stack of \(c_t\) has length at most \(H - d\). Let the assignment \(a\) satisfy the transition clause family of \(L\) with the current-label table \(\mathrm{la}\), the next-label table \(\mathrm{na}\) and the window table \(\mathrm{wa}\) of \(E\), for \(T\), \(H\) and the number \(N\) of situations. If \(X[t, \kappa(c_t)]\) is true under \(a\) and \(C[t, k, j, \gamma_{c_t}(k, j)]\) is true under \(a\) for all \(k < K\) and \(j < H\), then the variable \(X[t + 1, \kappa(c_{t+1})]\) is true under \(a\).

theorem upd_step_run {T H t : ℕ} {a : List Bool} (s : List (M.Γ M.k₀))
    (ha : cnfSat (Family.family E.layout E.la E.na E.wa T H E.N) 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))

Uses 22 · Used by 1

Statement usesThe transition 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 · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Window symbol code of a situation · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesIndex of a label/state variable · Good configurations · Label-and-state code of a configuration · The idle-extended step preserves good configurations · Situation index of a configuration · The table-driven row update · The table-driven step along a run · Update forcing (positive) · Truth of a variable under an assignment

Used byOne-step invariant

TheoremPushed-fill forcing#✓fully proved

Let \(L\) be a layout with \(A\) label/state variables, \(K\) stacks and \(g\) symbol codes, let \(\mathrm{sa}, \mathrm{pl}, \mathrm{cn}, \mathrm{pu}\) be situation tables and \(N, T, H \in \mathbb{N}\), and write \(W = A + KHg\), \(X[t, x] = tW + x\) and \(C[t, k, j, x] = tW + A + (kH + j)g + x\). If the assignment \(a\) satisfies the cell-shift family of these data, \(t < T\), \(i < N\), \(k < K\), \(j < \mathrm{pl}(i, k)\) and the variable \(X[t + 1, \mathrm{sa}(i)]\) is true under \(a\), then the variable \(C[t + 1, k, j, \mathrm{pu}(i, k, j)]\) is true under \(a\).

Only the situation literal is read.

theorem pf_force {L : Family.Layout} {sa : ℕ → ℕ} {pl cn : ℕ → ℕ → ℕ} {pu : ℕ → ℕ → ℕ → ℕ}
    {N T H : ℕ} {a : List Bool} (ha : cnfSat (Shift.shFamily L sa pl cn pu N T H) a)
    {t i k j : ℕ} (ht : t < T) (hi : i < N) (hk : k < L.KK) (hj : j < pl i k)
    (hS : Tr a (L.xIdx H (t + 1) (sa i))) : Tr a (L.cIdx H (t + 1) k j (pu i k j))

Uses 15 · Used by 1

Statement usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Index of a label/state variable · The cell-shift clause family · Truth of a variable under an assignment · Satisfaction of a dense CNF formula

Proof usesNumber of variables of the transition-clause formula · Dense clause from a list of literals · Literals of an overflow clause · Literals of a pushed-fill clause · The shift block of a situation and a stack · Literals of an in-range shift clause · L0 (a satisfied dense clause has a satisfied listed literal) · Dense CNF formula · Dense clause

Used byPushed-fill forcing for a good configuration

TheoremOverflow forcing#✓fully proved

Let \(L\) be a layout with \(K\) stacks, let \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\) and \(\mathrm{pu}\) be situation tables, and let \(a\) be an assignment satisfying the cell-shift clause family of \(L\) and these tables for bounds \(N\), \(T\) and \(H\). Write \(X[t, b]\) and \(C[t, k, j, x]\) for the label/state and cell variables at height \(H\). If \(t < T\), \(i < N\), \(k < K\), \(r < \mathrm{cn}(i, k) - \mathrm{pl}(i, k)\) and the situation variable \(X[t + 1, \mathrm{sa}(i)]\) is true under \(a\), then the variable \(C[t + 1, k, H - \mathrm{cn}(i, k) + \mathrm{pl}(i, k) + r, 0]\) is true under \(a\), where symbol code \(0\) is the empty cell. Subtraction is truncated at zero.

theorem ov_force {L : Family.Layout} {sa : ℕ → ℕ} {pl cn : ℕ → ℕ → ℕ} {pu : ℕ → ℕ → ℕ → ℕ}
    {N T H : ℕ} {a : List Bool} (ha : cnfSat (Shift.shFamily L sa pl cn pu N T H) a)
    {t i k r : ℕ} (ht : t < T) (hi : i < N) (hk : k < L.KK) (hr : r < cn i k - pl i k)
    (hS : Tr a (L.xIdx H (t + 1) (sa i))) :
    Tr a (L.cIdx H (t + 1) k (H - cn i k + pl i k + r) 0)

Uses 15 · Used by 1

Statement usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Index of a label/state variable · The cell-shift clause family · Truth of a variable under an assignment · Satisfaction of a dense CNF formula

Proof usesNumber of variables of the transition-clause formula · Dense clause from a list of literals · Literals of an overflow clause · Literals of a pushed-fill clause · The shift block of a situation and a stack · Literals of an in-range shift clause · L0 (a satisfied dense clause has a satisfied listed literal) · Dense CNF formula · Dense clause

Used byOverflow cells of the next row hold the table value

TheoremPushed-fill forcing for a good configuration#✓fully proved

Let \(E\) be an encoding of the machine \(M\) with \(K\) stacks and layout \(L\), let \(H \in \mathbb{N}\), let \(W\) be the row width of \(L\) at height \(H\), and write \(X[t, x] = tW + x\) for the label/state variables and \(C[t, k, j, x]\) for the cell variable of row \(t\), stack \(k\), depth \(j\) and symbol code \(x\). Let \(T, t \in \mathbb{N}\) with \(t < T\), let the assignment \(a\) satisfy the cell-shift family of \(E\) (tables \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\) and \(N\) situations) for \(T\) and \(H\), and let \(c\) be a good configuration with situation index \(i\) such that \(X[t + 1, \mathrm{sa}(i)]\) is true under \(a\). Then for all \(k < K\) and \(j < \mathrm{pl}(i, k)\) the variable \(C[t + 1, k, j, r]\) is true under \(a\), where \(r\) is the entry at stack \(k\) and depth \(j\) of the table-driven row update, at height \(H\) and for situation \(i\), of the cell codes of \(c\).

theorem pf_hold {T H t : ℕ} {a : List Bool}
    (ha : cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T H) a) (ht : t < T)
    (c : M.Cfg) (hc : E.Good c) (hS : Tr a (E.layout.xIdx H (t + 1) (E.sa (E.sitIdx c))))
    {k j : ℕ} (hk : k < E.KK) (hj : j < E.pl (E.sitIdx c) k) :
    Tr a (E.layout.cIdx H (t + 1) k j (E.tabRow H (E.sitIdx c) (E.cell c) k j))

Uses 22 · Used by 1

Statement usesIndex of a cell variable in the transition-family layout · Index of a label/state variable · The cell-shift clause family · Encoding data for a finite TM2 machine · Good configurations · Number of situations · Cell code of a configuration · Consumption table 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 · Situation index of a configuration · The table-driven row update · Truth of a variable under an assignment · Satisfaction of a dense CNF formula

Proof usesLabel-and-state code of a configuration · Label/state code of a situation · The situation index matches the code and windows · Window symbol code of a situation · Window depth of a machine · Pushed-fill forcing

Used byPushed-fill forcing on a real run

TheoremOverflow cells of the next row hold the table value#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with \(K\) stacks and window depth \(d\), and let \(a\) be an assignment satisfying the cell-shift clause family of \(E\)'s layout and tables \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\) for \(E\)'s number of situations and bounds \(T\) and \(H\). Write \(X[t, b]\) and \(C[t, k, j, x]\) for the label/state and cell variables at height \(H\). Let \(t < T\), let \(c\) be a configuration of \(M\) all of whose stack symbols have codes, suppose \(d \le H\), let \(i\) be the situation index of \(c\), and suppose \(X[t + 1, \mathrm{sa}(i)]\) is true under \(a\). Then for every \(k < K\) and every \(j\) with \(H - \max(\mathrm{pl}(i, k), \mathrm{cn}(i, k)) + \mathrm{pl}(i, k) \le j < H\), the variable \(C[t + 1, k, j, x]\) is true under \(a\), where \(x\) is the value at \((k, j)\) of the table-driven row update at height \(H\) of the cells of \(c\) for situation \(i\). Subtraction is truncated at zero.

At these depths the table-driven row update is \(0\), the empty cell.

theorem ov_hold {T H t : ℕ} {a : List Bool}
    (ha : cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T H) a) (ht : t < T)
    (c : M.Cfg) (hc : E.Good c) (hdH : depth M ≤ H)
    (hS : Tr a (E.layout.xIdx H (t + 1) (E.sa (E.sitIdx c))))
    {k j : ℕ} (hk : k < E.KK)
    (hj1 : H - max (E.pl (E.sitIdx c) k) (E.cn (E.sitIdx c) k) + E.pl (E.sitIdx c) k ≤ j)
    (hj2 : j < H) :
    Tr a (E.layout.cIdx H (t + 1) k j (E.tabRow H (E.sitIdx c) (E.cell c) k j))

Uses 28 · Used by 1

Statement usesIndex of a cell variable in the transition-family layout · Index of a label/state variable · The cell-shift clause family · Encoding data for a finite TM2 machine · Good configurations · Number of situations · Cell code of a configuration · Consumption table 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 · Situation index of a configuration · The table-driven row update · Truth of a variable under an assignment · Window depth of a machine · Satisfaction of a dense CNF formula

Proof usesLabel-and-state code of a configuration · Label/state code of a situation · Effect of a situation · The situation index matches the code and windows · Window symbol code of a situation · Decoded windows of a situation · Symbolic effect of a statement tree · The symbolic effect grows by at most the number of stack operations · Stack operations on a path of a statement tree · Overflow forcing · The situation step

Used byOverflow cells of the next row on a real run

TheoremPushed-fill forcing on a real run#✓fully proved

Let \(E\) be an encoding of the machine \(M\) with \(K\) stacks and layout \(L\), let \(d\) be the window depth of \(M\), let \(H \in \mathbb{N}\) with \(d \le H\), let \(W\) be the row width of \(L\) at height \(H\), and write \(X[t, x] = tW + x\) for the label/state variables and \(C[t, k, j, x]\) for the cell variable of row \(t\), stack \(k\), depth \(j\) and symbol code \(x\). Fix an input list \(s\), let \(c_n\) be the configuration after \(n\) steps of the idle-extended run of \(M\) from the initial configuration on \(s\), let \(T, t \in \mathbb{N}\) with \(t < T\), let \(i\) be the situation index of \(c_t\), and suppose every stack of \(c_t\) has length at most \(H - d\). Let the assignment \(a\) satisfy the cell-shift family of \(E\) (tables \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\) and \(N\) situations) for \(T\) and \(H\), and suppose \(X[t + 1, \mathrm{sa}(i)]\) is true under \(a\). Then for all \(k < K\) and \(j < \mathrm{pl}(i, k)\) the variable \(C[t + 1, k, j, x]\) is true under \(a\), where \(x\) is the code of the cell of \(c_{t+1}\) at stack \(k\) and depth \(j\) (code \(0\) if that cell is empty).

theorem pf_step_run {T H t : ℕ} {a : List Bool} (s : List (M.Γ M.k₀))
    (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)
    (hS : Tr a (E.layout.xIdx H (t + 1) (E.sa (E.sitIdx (runI M (initList M s) t)))))
    {k j : ℕ} (hk : k < E.KK) (hj : j < E.pl (E.sitIdx (runI M (initList M s) t)) k) :
    Tr a (E.layout.cIdx H (t + 1) k j (E.cell (runI M (initList M s) (t + 1)) k j))

Uses 31 · Used by 1

Statement usesIndex of a cell variable in the transition-family layout · Index of a label/state variable · The cell-shift clause family · Encoding data for a finite TM2 machine · Number of situations · Cell code of a configuration · Consumption table 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 · Situation index of a configuration · Truth of a variable under an assignment · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesGood configurations · Label-and-state code of a configuration · The idle-extended step preserves good configurations · Label/state code of a situation · Next label/state code of a situation · Pushed-fill forcing for a good configuration · Effect of a situation · The table-driven row update · The table-driven step along a run · Window symbol code of a situation · Decoded windows of a situation · Symbolic effect of a statement tree · The symbolic effect grows by at most the number of stack operations · Stack operations on a path of a statement tree · The situation step

Used byCell literals propagate one step along the real run

TheoremOverflow cells of the next row on a real run#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with \(K\) stacks and window depth \(d\), let \(s\) be an input, and let \(c_t\) be the configuration at step \(t\) of the idle-extended run of \(M\) from the initial configuration on input \(s\). Let \(a\) be an assignment satisfying the cell-shift clause family of \(E\)'s layout and tables \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\) for \(E\)'s number of situations and bounds \(T\) and \(H\), and write \(X[t, b]\) and \(C[t, k, j, x]\) for the label/state and cell variables at height \(H\). Suppose \(t < T\), every stack of \(c_t\) has length at most \(H - d\), \(d \le H\), and \(X[t + 1, \mathrm{sa}(i)]\) is true under \(a\), where \(i\) is the situation index of \(c_t\). Then for every \(k < K\) and every \(j\) with \(H - \max(\mathrm{pl}(i, k), \mathrm{cn}(i, k)) + \mathrm{pl}(i, k) \le j < H\), the variable \(C[t + 1, k, j, x]\) is true under \(a\), where \(x\) is the code of the cell of stack number \(k\) at depth \(j\) from the top in \(c_{t+1}\) (\(0\) if that cell is empty). Subtraction is truncated at zero.

theorem ov_step_run {T H t : ℕ} {a : List Bool} (s : List (M.Γ M.k₀))
    (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)
    (hS : Tr a (E.layout.xIdx H (t + 1) (E.sa (E.sitIdx (runI M (initList M s) t)))))
    {k j : ℕ} (hk : k < E.KK)
    (hj1 : H - max (E.pl (E.sitIdx (runI M (initList M s) t)) k)
      (E.cn (E.sitIdx (runI M (initList M s) t)) k) +
      E.pl (E.sitIdx (runI M (initList M s) t)) k ≤ j) (hj2 : j < H) :
    Tr a (E.layout.cIdx H (t + 1) k j (E.cell (runI M (initList M s) (t + 1)) k j))

Uses 25 · Used by 1

Statement usesIndex of a cell variable in the transition-family layout · Index of a label/state variable · The cell-shift clause family · Encoding data for a finite TM2 machine · Number of situations · Cell code of a configuration · Consumption table 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 · Situation index of a configuration · Truth of a variable under an assignment · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesGood configurations · Label-and-state code of a configuration · The idle-extended step preserves good configurations · Label/state code of a situation · Next label/state code of a situation · Overflow cells of the next row hold the table value · The table-driven row update · The table-driven step along a run · Window symbol code of a situation

Used byCell literals propagate one step along the real run

DefinitionStack cap#✓fully proved

For natural numbers \(m\), \(T\) and \(d\) (an input bound, a run length and a per-step growth), the stack cap is \(H = m + (T + 1) d + 1\).

It is used with \(d\) the window depth of the machine.

def capH (m T d : ℕ) : ℕ := m + (T + 1) * d + 1

Used by 23

Used byThe init generator at the stack cap · Stack-cap constraint 1 · Stack-cap constraint 2 · Stack heights are at most the cap minus the window depth · Init obligation, input pinned · The init family discharges the init obligation · One-step invariant at the stack cap · Row induction at the stack cap · Run tracking from the init obligation · Satisfying assignments yield accepting runs · A satisfying assignment tracks a certified run · No accepting certificate, no satisfying assignment · Completeness of the five clause families · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · Step bound of the host · The assembled generator, after the precomputation · Step budget of the counter program · The composed machine, raw input to formula · Target counter values · Every clause of the Cook–Levin formula has one slot per variable · Every NP problem reduces to binary-index CNF-SAT

TheoremStack heights along a run#✓fully proved

Let \(M\) be a finite TM2 machine with window depth \(d\), let \(c\) be a configuration and \(k\) a stack. For every \(t \in \mathbb{N}\), stack \(k\) of the configuration reached from \(c\) after \(t\) steps of the idle-extended run has length at most the length of stack \(k\) of \(c\) plus \(t \cdot d\).

theorem runI_height {M : FinTM2} (c : M.Cfg) (k : M.K) :
    ∀ t, ((runI M c t).stk k).length ≤ (c.stk k).length + t * depth M

Uses 4 · Used by 2

Statement usesWindow depth of a machine · Idle-extended run

Proof usesIdle-extended step · Stack heights grow by at most the window depth per step

Used byThe reduction machine halts with the emitted formula · Stack heights are at most the cap minus the window depth

TheoremStack heights are at most the cap minus the window depth#✓fully proved

Let \(M\) be a finite multi-stack Turing machine with window depth \(d\), let \(m\), \(T\) and \(t\) be natural numbers with \(t \le T\), and let \(s\) be an input of length at most \(m\). In the idle-extended run of \(M\) from the initial configuration on input \(s\), every stack of the configuration at step \(t\) has length at most \(H - d\), where \(H = m + (T + 1) d + 1\) is the stack cap for input bound \(m\), run length \(T\) and per-step growth \(d\).

theorem capH_height {M : FinTM2} {m T t : ℕ} (s : List (M.Γ M.k₀)) (hs : s.length ≤ m)
    (ht : t ≤ T) (k : M.K) :
    ((runI M (initList M s) t).stk k).length ≤ capH m T (depth M) - depth M

Uses 4 · Used by 3

Statement usesStack cap · Window depth of a machine · Idle-extended run

Proof usesStack heights along a run

Used byOne-step invariant at the stack cap · Row induction at the stack cap · Completeness of the five clause families

TheoremStack-cap constraint 1#✓fully proved

For natural numbers \(\ell\), \(m\), \(T\) and \(d\) with \(\ell \le m\), we have \(\ell + (T + 1) d \le H\), where \(H = m + (T + 1) d + 1\) is the stack cap for input bound \(m\), run length \(T\) and per-step growth \(d\).

theorem capH_c1 {l m T d : ℕ} (hl : l ≤ m) : l + (T + 1) * d ≤ capH m T d

Uses 1

Statement usesStack cap

TheoremStack-cap constraint 2#✓fully proved

For natural numbers \(m\), \(T\) and \(d\) with \(T \ge 1\), the stack cap \(H = m + (T + 1) d + 1\) for input bound \(m\), run length \(T\) and per-step growth \(d\) satisfies \(2d \le H\).

theorem capH_c2 {m T d : ℕ} (hT : 1 ≤ T) : 2 * d ≤ capH m T d

Uses 1

Statement usesStack cap

TheoremThe three depth regions cover every depth exactly once#✓fully proved

Let \(p, q, H, j\) be natural numbers with \(j < H\), and let \(m = H - \max(p, q) + p\), where the subtraction is truncated at \(0\). Then \(j\) lies in exactly one of the ranges \(j < p\) (pushed fill), \(p \le j < m\) (in-range shift) and \(m \le j < H\) (overflow).

These are the depth hypotheses of the pushed-fill, in-range shift and overflow lemmas; nothing is assumed about \(p\), \(q\) and \(H\).

theorem region_cover (p q H j : ℕ) (hj : j < H) :
    (j < p ∨ (p ≤ j ∧ j < H - max p q + p) ∨ (H - max p q + p ≤ j ∧ j < H)) ∧
    ¬ (j < p ∧ p ≤ j) ∧ ¬ (j < p ∧ H - max p q + p ≤ j) ∧
    ¬ (j < H - max p q + p ∧ H - max p q + p ≤ j)

Used by 1

Used byCell literals propagate one step along the real run

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.