Entries of a decoded stack on prefix-form input to Positive shift step on a real run (L3⁺)

TheoremEntries of a decoded stack on prefix-form input#✓fully proved

Let \(f : \mathbb{N} \to \mathrm{Option}\,\alpha\) and write \(\bot\) for the absent value. For \(j, m \in \mathbb{N}\) let \(\mathrm{decS}(f, j, m)\) be the list of the values \(f(j), f(j + 1), \dots\), read for at most \(m\) positions and stopped at the first \(\bot\). Suppose \(f\) is in prefix form on the window from \(j\) to \(j + m\): whenever \(j \le a \le b < j + m\) and \(f(a) = \bot\), also \(f(b) = \bot\). Then for every \(i < m\), the \(i\)-th entry of \(\mathrm{decS}(f, j, m)\), taken to be \(\bot\) when the list has at most \(i\) entries, equals \(f(j + i)\).

theorem getElem?_decS (f : ℕ → Option α) : ∀ (j m : ℕ),
    (∀ a b, j ≤ a → a ≤ b → b < j + m → f a = none → f b = none) →
    ∀ i < m, (decS f j m)[i]? = f (j + i)

Uses 1 · Used by 1

Statement usesReading a list from a sequence of cells

Used byC1b (decoding a well-formed row loses nothing)

TheoremStack heights grow by at most the window depth per step#✓fully proved

Let \(M\) be a finite multi-stack Turing machine (finitely many stacks, labels and states, and a finite input alphabet), and let \(d\) be its window depth, the largest number of push, peek and pop nodes on a root-to-leaf path of any of its statement trees. For every configuration \(c\) of \(M\) and every stack \(k\), the length of stack \(k\) after one idle-extended step of \(M\) from \(c\) is at most the length of stack \(k\) of \(c\) plus \(d\).

theorem stepI_height {M : FinTM2} (c : M.Cfg) (k : M.K) :
    ((stepI M c).stk k).length ≤ (c.stk k).length + depth M

Uses 9 · Used by 2

Statement usesWindow depth of a machine · Idle-extended step

Proof usesApplying an effect to the original stacks · 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 · The idle-extended step is the situation step applied to the stacks · Windows of a configuration

Used byC2' (decoding the table-driven row gives the next configuration) · Stack heights along a run

DefinitionC1 decoder (decoding a row)#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(H, n \in \mathbb{N}\), and let \(w : \mathbb{N} \to \mathbb{N} \to \mathbb{N}\). The decoded configuration has the label and the state that the inverse (label, state) numbering of \(E\) assigns to \(n\). For each stack \(k\) of \(M\), with stack number \(\kappa\), the decoded stack \(k\) lists, from the top, the symbols of stack \(k\) with codes \(w(\kappa, 0), w(\kappa, 1), \dots\), stopping before the first \(j\) at which \(w(\kappa, j)\) is \(0\) or is not a valid code of stack \(k\), and taking at most \(H\) symbols. The valid codes of stack \(k\) are \(1, \dots, s\), where \(s\) is the size of its effective alphabet, and code \(i + 1\) stands for symbol number \(i\) of that alphabet, counting from \(0\).

def decRow (H n : ℕ) (w : ℕ → ℕ → ℕ) : M.Cfg :=
  ⟨(E.ld n).1, (E.ld n).2, fun k => decS (fun j => E.decO k (w (E.kc k) j)) 0 H⟩

Uses 3 · Used by 6

Statement usesEncoding data for a finite TM2 machine · Decoding a symbol code · Reading a list from a sequence of cells

Used byC1e (the row decoder reads only the window) · C1a (decoding recovers a good configuration) · C1d (decoded configurations are good) · C2' (decoding the table-driven row gives the next configuration) · C1b (decoding a well-formed row loses nothing) · Good configurations are determined by their row (C1f)

DefinitionWell-formed rows of cells#✓fully proved

Let \(M\) be a finite multi-stack Turing machine and \(E\) an encoding of \(M\) with \(K\) numbered stacks, let \(H \in \mathbb{N}\), and let \(w : \mathbb{N} \to \mathbb{N} \to \mathbb{N}\) assign a code \(w(k, j)\) to each stack number \(k\) and depth \(j\). The row \(w\) is well formed at height \(H\) when for every \(k < K\) and every \(j < H\): \(w(k, j)\) is at most the size of the effective alphabet of the stack numbered \(k\), and if \(w(k, j) = 0\) then \(w(k, b) = 0\) for every \(b\) with \(j \le b < H\).

Code \(0\) is the empty cell, so the second condition says that each stack is in prefix form.

def RowOK (H : ℕ) (w : ℕ → ℕ → ℕ) : Prop :=
  ∀ k < E.KK, ∀ j < H, w k j ≤ E.sz (E.kd k) ∧ (w k j = 0 → ∀ b, j ≤ b → b < H → w k b = 0)

Uses 1 · Used by 2

Statement usesEncoding data for a finite TM2 machine

Used byC1c (cell arrays of good configurations are well-formed rows) · C1b (decoding a well-formed row loses nothing)

TheoremC1a (decoding recovers a good configuration)#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(H \in \mathbb{N}\), and let \(c\) be a good configuration of \(M\) (every symbol on every stack of \(c\) lies in the effective alphabet of \(E\)) all of whose stacks have length at most \(H\). Then the row decoder of \(E\) at height \(H\), applied to the (label, state) code of \(c\) and the cell array of \(c\), returns \(c\).

theorem decRow_enc (H : ℕ) (c : M.Cfg) (hc : E.Good c) (hh : ∀ k, (c.stk k).length ≤ H) :
    E.decRow H (E.code c) (E.cell c) = c

Uses 8 · Used by 2

Statement usesEncoding data for a finite TM2 machine · Good configurations · Cell code of a configuration · Label-and-state code of a configuration · C1 decoder (decoding a row)

Proof usesDecoding a symbol code · Reading a list from a sequence of cells · Reading back a list from its cells

Used byC2' (decoding the table-driven row gives the next configuration) · Good configurations are determined by their row (C1f)

TheoremC1b (decoding a well-formed row loses nothing)#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with \(K\) numbered stacks and \(A_0\) (label, state) codes, let \(H \in \mathbb{N}\), let \(n < A_0\), and let \(w : \mathbb{N} \to \mathbb{N} \to \mathbb{N}\) be a well-formed row of height \(H\): for all \(k < K\) and \(j < H\), \(w(k, j)\) is at most the size of the effective alphabet of stack number \(k\), and if \(w(k, j) = 0\) then \(w(k, b) = 0\) for every \(b\) with \(j \le b < H\). Let \(c\) be the configuration that the row decoder of \(E\) at height \(H\) returns on code \(n\) and array \(w\). Then the (label, state) code of \(c\) is \(n\), and the cell code of \(c\) at stack number \(k\) and depth \(j\) equals \(w(k, j)\) for all \(k < K\) and \(j < H\).

theorem enc_decRow (H n : ℕ) (hn : n < E.A0) (w : ℕ → ℕ → ℕ) (hw : E.RowOK H w) :
    E.code (E.decRow H n w) = n ∧ ∀ k < E.KK, ∀ j < H, E.cell (E.decRow H n w) k j = w k j

Uses 8

Statement usesEncoding data for a finite TM2 machine · Well-formed rows of cells · Cell code of a configuration · Label-and-state code of a configuration · C1 decoder (decoding a row)

Proof usesDecoding a symbol code · Reading a list from a sequence of cells · Entries of a decoded stack on prefix-form input

TheoremC1c (cell arrays of good configurations are well-formed rows)#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with \(K\) numbered stacks, and let \(c\) be a good configuration of \(M\), that is, every symbol on every stack of \(c\) lies in the effective alphabet of \(E\). Let \(w\) be the cell array of \(c\): \(w(k, j)\) is the code of the symbol at depth \(j\) from the top of stack number \(k\), or \(0\) if there is none. Then for every \(H \in \mathbb{N}\), \(w\) is a well-formed row of height \(H\): for all \(k < K\) and \(j < H\), the code \(w(k, j)\) is at most the size of the effective alphabet of stack number \(k\), and if \(w(k, j) = 0\) then \(w(k, b) = 0\) for every \(b\) with \(j \le b < H\).

theorem cell_rowOK (H : ℕ) (c : M.Cfg) (hc : E.Good c) : E.RowOK H (E.cell c)

Uses 4

Statement usesEncoding data for a finite TM2 machine · Good configurations · Well-formed rows of cells · Cell code of a configuration

TheoremC1d (decoded configurations are good)#✓fully proved

Let \(E\) be an encoding of a machine \(M\). For all \(H, n \in \mathbb{N}\) and every \(w : \mathbb{N} \to \mathbb{N} \to \mathbb{N}\), the configuration that the row decoder of \(E\) at height \(H\) returns on code \(n\) and array \(w\) is good: every symbol on each of its stacks lies in the effective alphabet of \(E\).

theorem decRow_good (H n : ℕ) (w : ℕ → ℕ → ℕ) : E.Good (E.decRow H n w)

Uses 5

Statement usesEncoding data for a finite TM2 machine · Good configurations · C1 decoder (decoding a row)

Proof usesDecoding a symbol code · Reading a list from a sequence of cells

TheoremC1e (the row decoder reads only the window)#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with \(K\) numbered stacks, let \(H, n \in \mathbb{N}\), and let \(w, w' : \mathbb{N} \to \mathbb{N} \to \mathbb{N}\). If \(w(k, j) = w'(k, j)\) for all \(k < K\) and \(j < H\), then the row decoder of \(E\) at height \(H\) returns the same configuration on code \(n\) and array \(w\) as on code \(n\) and array \(w'\).

theorem decRow_congr (H n : ℕ) (w w' : ℕ → ℕ → ℕ) (h : ∀ k < E.KK, ∀ j < H, w k j = w' k j) :
    E.decRow H n w = E.decRow H n w'

Uses 4 · Used by 2

Statement usesEncoding data for a finite TM2 machine · C1 decoder (decoding a row)

Proof usesDecoding a symbol code · Reading a list from a sequence of cells

Used byC2' (decoding the table-driven row gives the next configuration) · Good configurations are determined by their row (C1f)

TheoremGood configurations are determined by their row (C1f)#✓fully proved

Let \(M\) be a finite multi-stack Turing machine and \(E\) an encoding of \(M\) with \(K\) numbered stacks, let \(H \in \mathbb{N}\), and for a configuration \(c\) write \(\mathrm{cell}(c, k, j)\) for the code of the symbol at depth \(j\) of the stack numbered \(k\) (\(0\) if there is none). Let \(c\) and \(c'\) be configurations that are good for \(E\) (every stack symbol lies in the effective alphabet of its stack) and all of whose stacks have length at most \(H\). If \(c\) and \(c'\) have the same (label, state) code and \(\mathrm{cell}(c, k, j) = \mathrm{cell}(c', k, j)\) for all \(k < K\) and \(j < H\), then \(c = c'\).

theorem row_inj (H : ℕ) (c c' : M.Cfg) (hc : E.Good c) (hc' : E.Good c')
    (hh : ∀ k, (c.stk k).length ≤ H) (hh' : ∀ k, (c'.stk k).length ≤ H)
    (hcode : E.code c = E.code c') (hcell : ∀ k < E.KK, ∀ j < H, E.cell c k j = E.cell c' k j) :
    c = c'

Uses 7

Statement usesEncoding data for a finite TM2 machine · Good configurations · Cell code of a configuration · Label-and-state code of a configuration

Proof usesC1 decoder (decoding a row) · C1e (the row decoder reads only the window) · C1a (decoding recovers a good configuration)

TheoremC2' (decoding the table-driven row gives the next configuration)#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with window depth \(d\), let \(H \ge d\) be a natural number, and let \(c\) be a good configuration of \(M\) (every symbol on every stack of \(c\) lies in the effective alphabet of \(E\)) all of whose stacks have length at most \(H - d\). Let \(i\) be the situation index of \(c\). Then the row decoder of \(E\) at height \(H\), applied to the next (label, state) code of situation \(i\) and to the table-driven row update at height \(H\) of situation \(i\) on the cell array of \(c\), returns the idle-extended step of \(c\): the configuration after one step of \(M\), or \(c\) itself if \(c\) is halted.

theorem decRow_tabRow (H : ℕ) (hH : depth M ≤ H) (c : M.Cfg) (hc : E.Good c)
    (hh : ∀ k, (c.stk k).length ≤ H - depth M) :
    E.decRow H (E.na (E.sitIdx c)) (E.tabRow H (E.sitIdx c) (E.cell c)) = stepI M c

Uses 15

Statement usesEncoding data for a finite TM2 machine · Good configurations · Cell code of a configuration · C1 decoder (decoding a row) · Next label/state code of a situation · Situation index of a configuration · The table-driven row update · Window depth of a machine · Idle-extended step

Proof usesLabel-and-state code of a configuration · C1e (the row decoder reads only the window) · C1a (decoding recovers a good configuration) · The idle-extended step preserves good configurations · The table-driven step · Stack heights grow by at most the window depth per step

DefinitionTruth of a variable under an assignment#✓fully proved

For an assignment \(a\), given as a list of booleans, and a variable index \(v \in \mathbb{N}\), the variable \(v\) is true under \(a\) when \(v\) is less than the length of \(a\) and the entry of \(a\) at position \(v\) is true. In particular, variables with index at least the length of \(a\) are not true.

def Tr (a : List Bool) (v : ℕ) : Prop := a[v]? = some true

Used by 27

Used byCell block of a row equal to an array · Cell literals of an array hold in a row · In-range shift forcing (L1) · Positive core of the shift step (L2⁺) · Exact shift step (L2) · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · The code of a configuration holds in a row · Transition clauses force the next label · Transition clauses force the next label, stack-and-depth form · Overflow forcing · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · L2 (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 · Positive dense unit clauses force their variable · Accept-cell clauses pin the top output symbol · Accept-code clauses pin the (label, state) code · The all-true assignment violates the accept family

TheoremL0 (a satisfied dense clause has a satisfied listed literal)#✓fully proved

Let \(V \in \mathbb{N}\), let \(\ell\) be a list of pairs \((p, b)\) of a variable index \(p \in \mathbb{N}\) and a sign \(b\) (true or false), and let \(a\) be a list of booleans. If \(a\) satisfies the dense clause over \(V\) variables built from \(\ell\), then some pair \((p, b) \in \ell\) has \(p\) less than the length of \(a\) and \(a_p = b\).

theorem clauseSat_dense {V : ℕ} {ls : List (ℕ × Bool)} {a : List Bool}
    (h : clauseSat (Family.denseClause V ls) a) : ∃ p b, (p, b) ∈ ls ∧ a[p]? = some b

Uses 3 · Used by 9

Statement usesDense clause from a list of literals · Satisfaction of a dense clause

Proof usesDense clause

Used byIn-range shift forcing (L1) · Transition clauses force the next label · Overflow forcing · Pushed-fill forcing · Init semantics · Positive dense unit clauses force their variable · Accept-cell clauses pin the top output symbol · Accept-code clauses pin the (label, state) code · Exact clause semantics

TheoremIn-range shift forcing (L1)#✓fully proved

Let \(L\) be a layout with \(K\) stacks and \(g\) symbol codes, let \(sa\), \(pl\), \(cn\), \(pu\) be situation tables and \(N, T, H \in \mathbb{N}\), and let \(a\) be an assignment satisfying the cell-shift clause family of \(L\) with these tables and bounds \(N\), \(T\), \(H\). Call a variable true when its index is less than the length of \(a\) and \(a\) is true there. Write \(S[t, i]\) for the label/state variable \(sa(i)\) of row \(t + 1\) and \(C[t, k, j, x]\) for the cell variable of row \(t\), stack \(k\), depth \(j\) and symbol code \(x\) (both at height \(H\)). Let \(t < T\), \(i < N\), \(k < K\), \(x < g\) and \(u < H - \max(pl(i, k), cn(i, k))\), with truncated subtraction. If \(S[t, i]\) and \(C[t, k, u + cn(i, k), x]\) are true, then \(C[t + 1, k, u + pl(i, k), x]\) is true.

theorem sh_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 u x : ℕ} (ht : t < T) (hi : i < N) (hk : k < L.KK)
    (hu : u < H - max (pl i k) (cn i k)) (hx : x < L.g)
    (hS : Tr a (L.xIdx H (t + 1) (sa i))) (hC : Tr a (L.cIdx H t k (u + cn i k) x)) :
    Tr a (L.cIdx H (t + 1) k (u + pl i k) x)

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 byPositive core of the shift step (L2⁺)

DefinitionCell block of a row equal to an array#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with \(K\) numbered stacks and \(g\) symbol codes, let \(a\) be a list of booleans, let \(H, t \in \mathbb{N}\), and let \(w : \mathbb{N} \to \mathbb{N} \to \mathbb{N}\). The cell block of row \(t\) is exactly \(w\) under \(a\) when, for all \(k < K\), \(j < H\) and \(x < g\), the cell variable for time \(t\), stack \(k\), depth \(j\) and symbol code \(x\) in the layout of \(E\) at height \(H\) is true under \(a\) if and only if \(x = w(k, j)\). A variable \(v\) is true under \(a\) when \(v\) is less than the length of \(a\) and the entry of \(a\) at position \(v\) is true.

def CellsAre (a : List Bool) (H t : ℕ) (w : ℕ → ℕ → ℕ) : Prop :=
  ∀ k < E.KK, ∀ j < H, ∀ x < E.g, Tr a (E.layout.cIdx H t k j x) ↔ x = w k j

Uses 5 · Used by 2

Statement usesIndex of a cell variable in the transition-family layout · Encoding data for a finite TM2 machine · Symbol-code bound · Clause layout of a machine encoding · Truth of a variable under an assignment

Used byExact shift step (L2) · Exact shift step on a real run (L3)

DefinitionCell literals of an array hold in a row#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with \(K\) numbered stacks, let \(a\) be a list of booleans, let \(H, t \in \mathbb{N}\), and let \(w : \mathbb{N} \to \mathbb{N} \to \mathbb{N}\). The cell literals of \(w\) hold in row \(t\) under \(a\) when, for all \(k < K\) and \(j < H\), the cell variable for time \(t\), stack \(k\), depth \(j\) and symbol code \(w(k, j)\) in the layout of \(E\) at height \(H\) is true under \(a\), that is, its index is less than the length of \(a\) and the entry of \(a\) at that index is true.

Unlike the exact form, this says nothing about the cell variables for other symbol codes.

def CellsHold (a : List Bool) (H t : ℕ) (w : ℕ → ℕ → ℕ) : Prop :=
  ∀ k < E.KK, ∀ j < H, Tr a (E.layout.cIdx H t k j (w k j))

Uses 4 · Used by 17

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

Used byPositive core of the shift step (L2⁺) · Positive shift step on a real run (L3⁺) · L2 (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

TheoremPositive core of the shift step (L2⁺)#✓fully proved

Let \(M\) be a finite multi-stack Turing machine and \(E\) an encoding of \(M\) with \(K\) numbered stacks, tables \(sa\), \(pl\), \(cn\), \(pu\) and \(N\) situations, let \(T, H, t \in \mathbb{N}\) with \(t < T\), and let \(a\) be an assignment satisfying the cell-shift clause family of the layout of \(E\) with these tables and bounds \(N\), \(T\), \(H\). Call a variable true when its index is less than the length of \(a\) and \(a\) is true there. Write \(S[t, i]\) for the label/state variable \(sa(i)\) of row \(t + 1\), \(C[t, k, j, x]\) for the cell variable of row \(t\), stack \(k\), depth \(j\) and symbol code \(x\) (both at height \(H\)), and \(\mathrm{cell}(c, k, j)\) for the code at depth \(j\) of the stack numbered \(k\) of a configuration \(c\) (\(0\) if there is none). Let \(c\) be a configuration that is good for \(E\) (every stack symbol lies in the effective alphabet of its stack), with situation index \(i\). Suppose that \(C[t, k', j', \mathrm{cell}(c, k', j')]\) is true for all \(k' < K\) and \(j' < H\), and that \(S[t, i]\) is true. Then for every \(k < K\) and every \(j\) with \(pl(i, k) \le j < H - \max(pl(i, k), cn(i, k)) + pl(i, k)\) (truncated subtraction), the variable \(C[t + 1, k, j, R(k, j)]\) is true, where \(R\) is the table-driven row update at height \(H\) of the cells of \(c\) for situation \(i\).

theorem sh_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) (hrow : E.CellsHold a H t (E.cell c))
    (hS : Tr a (E.layout.xIdx H (t + 1) (E.sa (E.sitIdx c))))
    {k j : ℕ} (hk : k < E.KK) (hj1 : E.pl (E.sitIdx c) k ≤ j)
    (hj2 : j < H - max (E.pl (E.sitIdx c) k) (E.cn (E.sitIdx c) k) + 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 25 · Used by 2

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 · Cell literals of an array hold in a row · 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 · Symbol-code bound · The symbol-code bound is positive · 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 · In-range shift forcing (L1)

Used byExact shift step (L2) · Positive shift step on a real run (L3⁺)

TheoremExact shift step (L2)#✓fully proved

Let \(M\) be a finite multi-stack Turing machine and \(E\) an encoding of \(M\) with \(K\) numbered stacks, \(g\) symbol codes, tables \(sa\), \(pl\), \(cn\), \(pu\) and \(N\) situations, let \(T, H, t \in \mathbb{N}\) with \(t < T\), and let \(a\) be an assignment satisfying the cell-shift clause family of the layout of \(E\) with these tables and bounds \(N\), \(T\), \(H\). Call a variable true when its index is less than the length of \(a\) and \(a\) is true there. Write \(S[t, i]\) for the label/state variable \(sa(i)\) of row \(t + 1\), \(C[t, k, j, x]\) for the cell variable of row \(t\), stack \(k\), depth \(j\) and symbol code \(x\) (both at height \(H\)), and \(\mathrm{cell}(c, k, j)\) for the code at depth \(j\) of the stack numbered \(k\) of a configuration \(c\) (\(0\) if there is none). Let \(c\) be a configuration that is good for \(E\) (every stack symbol lies in the effective alphabet of its stack), with situation index \(i\). Suppose that for all \(k' < K\), \(j' < H\) and \(x < g\) the variable \(C[t, k', j', x]\) is true exactly when \(x = \mathrm{cell}(c, k', j')\), and that \(S[t, i]\) is true. Let \(k < K\) and \(pl(i, k) \le j < H - \max(pl(i, k), cn(i, k)) + pl(i, k)\) (truncated subtraction), and suppose at most one \(x < g\) makes \(C[t + 1, k, j, x]\) true. Then for every \(x < g\), \(C[t + 1, k, j, x]\) is true exactly when \(x = R(k, j)\), where \(R\) is the table-driven row update at height \(H\) of the cells of \(c\) for situation \(i\).

theorem sh_step_cell {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) (hrow : E.CellsAre a H t (E.cell c))
    (hS : Tr a (E.layout.xIdx H (t + 1) (E.sa (E.sitIdx c))))
    {k j : ℕ} (hk : k < E.KK) (hj1 : E.pl (E.sitIdx c) k ≤ j)
    (hj2 : j < H - max (E.pl (E.sitIdx c) k) (E.cn (E.sitIdx c) k) + E.pl (E.sitIdx c) k)
    (hamo : ∀ x < E.g, ∀ y < E.g, Tr a (E.layout.cIdx H (t + 1) k j x) →
      Tr a (E.layout.cIdx H (t + 1) k j y) → x = y) :
    ∀ x < E.g, Tr a (E.layout.cIdx H (t + 1) k j x) ↔
      x = E.tabRow H (E.sitIdx c) (E.cell c) k j

Uses 20 · 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 · Cell block of a row equal to an array · Good configurations · Number of situations · Cell code of a configuration · Consumption table of a situation · Symbol-code bound · 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 usesThe symbol-code bound is positive · Positive core of the shift step (L2⁺)

Used byExact shift step on a real run (L3)

TheoremExact shift step on a real run (L3)#✓fully proved

Let \(M\) be a finite multi-stack Turing machine and \(E\) an encoding of \(M\) with \(K\) numbered stacks, \(g\) symbol codes, tables \(sa\), \(pl\), \(cn\), \(pu\) and \(N\) situations, let \(T, H, t \in \mathbb{N}\) with \(t < T\), and let \(a\) be an assignment satisfying the cell-shift clause family of the layout of \(E\) with these tables and bounds \(N\), \(T\), \(H\). Call a variable true when its index is less than the length of \(a\) and \(a\) is true there. Write \(S[t, i]\) for the label/state variable \(sa(i)\) of row \(t + 1\), \(C[t, k, j, x]\) for the cell variable of row \(t\), stack \(k\), depth \(j\) and symbol code \(x\) (both at height \(H\)), and \(\mathrm{cell}(c, k, j)\) for the code at depth \(j\) of the stack numbered \(k\) of a configuration \(c\) (\(0\) if there is none). Fix an input list \(s\), let \(c_n\) be the configuration after \(n\) idle-extended steps of \(M\) from the initial configuration on \(s\), and let \(i\) be the situation index of \(c_t\). Suppose that every stack of \(c_t\) has length at most \(H - d\), where \(d\) is the window depth of \(M\), that for all \(k' < K\), \(j' < H\) and \(x < g\) the variable \(C[t, k', j', x]\) is true exactly when \(x = \mathrm{cell}(c_t, k', j')\), and that \(S[t, i]\) is true. Let \(k < K\) and \(pl(i, k) \le j < H - \max(pl(i, k), cn(i, k)) + pl(i, k)\), and suppose at most one \(x < g\) makes \(C[t + 1, k, j, x]\) true. Then for every \(x < g\), \(C[t + 1, k, j, x]\) is true exactly when \(x = \mathrm{cell}(c_{t+1}, k, j)\). Subtraction is truncated at \(0\).

No row is decoded in the proof.

theorem sh_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)
    (hrow : E.CellsAre a H t (E.cell (runI M (initList M s) t)))
    (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 : 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)
    (hamo : ∀ x < E.g, ∀ y < E.g, Tr a (E.layout.cIdx H (t + 1) k j x) →
      Tr a (E.layout.cIdx H (t + 1) k j y) → x = y) :
    ∀ x < E.g, Tr a (E.layout.cIdx H (t + 1) k j x) ↔
      x = E.cell (runI M (initList M s) (t + 1)) k j

Uses 27

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 · Cell block of a row equal to an array · Number of situations · Cell code of a configuration · Consumption table of a situation · Symbol-code bound · 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 · Exact shift step (L2) · The table-driven row update · The table-driven step along a run · Window symbol code of a situation

TheoremPositive shift step on a real run (L3⁺)#✓fully proved

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

theorem sh_step_run_pos {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)
    (hrow : E.CellsHold a H t (E.cell (runI M (initList M s) t)))
    (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 : 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 26 · Used by 2

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 · Cell literals of an array hold in a row · 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 · Positive core of the shift step (L2⁺) · The table-driven row update · The table-driven step along a run · Window symbol code of a situation

Used byComposition with the shift family · Cell 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.