Applying an effect to the original stacks to Reading back a list from its cells

DefinitionApplying an effect to the original stacks#✓fully proved

Let \(S_0\) assign a list \(S_0(k)\) to each stack \(k\), and let \(r = (\ell, v, P, c)\) consist of a label \(\ell\) (possibly the halted label), a state \(v\), a list \(P(k)\) for each stack \(k\) and a natural number \(c(k)\) for each stack \(k\). This is the configuration with label \(\ell\), state \(v\), and stack \(k\) equal to \(P(k)\) followed by \(S_0(k)\) with its first \(c(k)\) symbols (from the top) removed.

Applied to an effect, \(P(k)\) is the pushed prefix still on top of stack \(k\) and \(c(k)\) is the net number of original symbols consumed.

def applyEff (S0 : ∀ k, List (Γ k)) (r : Option Λ × σ × (∀ k, List (Γ k)) × (K → ℕ)) :
    TM2.Cfg Γ Λ σ :=
  ⟨r.1, r.2.1, fun k => r.2.2.1 k ++ (S0 k).drop (r.2.2.2 k)⟩

Used by 5

Used byThe symbolic effect of a statement agrees with the real step · The idle-extended step preserves good configurations · The idle-extended step is the situation step applied to the stacks · The table-driven step · Stack heights grow by at most the window depth per step

TheoremReading the top through the windows#✓fully proved

Let \(d \in \mathbb{N}\), let \(S_0\) and \(P\) assign a list to each stack, let \(c\) assign a natural number to each stack, and let \(k\) be a stack with \(c(k) < d\). Reading the top of stack \(k\) from the depth-\(d\) windows of the lists \(S_0\), with pushed symbols \(P\) and consumption counts \(c\), gives the first symbol of \(P(k)\) followed by \(S_0(k)\) with its first \(c(k)\) symbols removed, or ⊥ if that list is empty.

theorem readTop_eq (d : ℕ) (S0 P : ∀ k, List (Γ k)) (c : K → ℕ) (k : K) (hc : c k < d) :
    readTop (fun k => window d (S0 k)) P c k = (P k ++ (S0 k).drop (c k)).head?

Uses 2 · Used by 1

Statement usesTop of a stack as read from the windows · Top window of a stack

Used byThe symbolic effect of a statement agrees with the real step

TheoremThe symbolic effect of a statement agrees with the real step#✓fully proved

Let \(q\) be a statement tree of a multi-stack machine, \(d \in \mathbb{N}\), and \(S_0\) an assignment of a list \(S_0(k)\) to each stack \(k\). Let \(v\) be a state, \(P\) an assignment of a list \(P(k)\) to each stack, and \(c\) an assignment of a natural number \(c(k)\) to each stack with \(c(k) + \operatorname{ops}(q) \le d\) for every \(k\). Then running \(q\) from state \(v\) on the stacks whose stack \(k\) is \(P(k)\) followed by \(S_0(k)\) with its first \(c(k)\) symbols removed gives the configuration obtained by applying to \(S_0\) the effect of \(q\) computed from \(v\), \(P\), \(c\) and the depth-\(d\) windows of the \(S_0(k)\).

Here \(\operatorname{ops}(q)\) is the largest number of push, peek and pop nodes on a path of \(q\), so the hypothesis keeps every read inside the windows.

theorem eff_agree (d : ℕ) (S0 : ∀ k, List (Γ k)) (q : TM2.Stmt Γ Λ σ) :
    ∀ (v : σ) (P : ∀ k, List (Γ k)) (c : K → ℕ), (∀ k, c k + ops q ≤ d) →
      TM2.stepAux q v (fun k => P k ++ (S0 k).drop (c k)) =
        applyEff S0 (eff (fun k => window d (S0 k)) q v P c)

Uses 6 · Used by 1

Statement usesApplying an effect to the original stacks · Symbolic effect of a statement tree · Stack operations on a path of a statement tree · Top window of a stack

Proof usesTop of a stack as read from the windows · Reading the top through the windows

Used byThe idle-extended step is the situation step applied to the stacks

DefinitionIdle-extended step#✓fully proved

For a finite TM2 machine \(M\) and a configuration \(c\), the idle-extended step of \(M\) at \(c\) is the configuration that one step of \(M\) produces from \(c\) when the label of \(c\) is not the halted label, and is \(c\) itself when it is (a halted configuration stays put).

def stepI (M : FinTM2) (c : M.Cfg) : M.Cfg := (TM2.step M.m c).getD c

Used by 11

Used byThe idle-extended step preserves good configurations · Idle-extended run · The idle-extended step is the situation step applied to the stacks · The table-driven step · C2' (decoding the table-driven row gives the next configuration) · Stack heights grow by at most the window depth per step · Stack heights along a run · Unfolding the idle-extended run from the front · The idle-extended run stays at the halting configuration · A halted configuration is fixed by the idle-extended run · The idle-extended run follows the real run

DefinitionIdle-extended run#✓fully proved

For a finite TM2 machine \(M\) and a configuration \(c\), the idle-extended run of \(M\) from \(c\) is the sequence of configurations whose term at time \(0\) is \(c\) and whose term at time \(t + 1\) is the idle-extended step of \(M\) applied to its term at time \(t\).

def runI (M : FinTM2) (c : M.Cfg) : ℕ → M.Cfg
  | 0 => c
  | t + 1 => stepI M (runI M c t)

Uses 1 · Used by 37

Statement usesIdle-extended step

Used byCorrectness of the reduction · The verifier's run settles on its output · The reduction machine halts with the emitted formula · The table-driven step along a run · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · Stack heights are at most the cap minus the window depth · Overflow cells of the next row on a real run · Pushed-fill forcing on a real run · Stack heights along a run · L3 (S-definition, real run) · Composition with the shift family · Update forcing, real run · Cell literals propagate one step along the real run · One-step invariant at the stack cap · One-step invariant · 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 · Unfolding the idle-extended run from the front · No accepting certificate, no satisfying assignment · Completeness of the accept family · Completeness of the five clause families · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · Row-0 cells of the start configuration are run literals · The idle-extended run stays at the halting configuration · A halted configuration is fixed by the idle-extended run · The idle-extended run follows the real run · The real run's literals · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · The run assignment satisfies the update family · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · Correctness of the assembled formula

DefinitionWindows of a configuration#✓fully proved

Let \(M\) be a finite TM2 machine with window depth \(d\) and let \(c\) be a configuration. The window of \(c\) on stack \(k\) is the list of length \(d\) whose entry at position \(j < d\) is the symbol at depth \(j\) of stack \(k\) (counted from the top, starting at \(0\)) when the stack has more than \(j\) symbols, and the empty cell \(\bot\) otherwise.

def winC (M : FinTM2) (c : M.Cfg) : ∀ k, List (Option (M.Γ k)) :=
  fun k => window (depth M) (c.stk k)

Uses 2 · Used by 4

Statement usesWindow depth of a machine · Top window of a stack

Used byThe idle-extended step preserves good configurations · The idle-extended step is the situation step applied to the stacks · The table-driven step · Stack heights grow by at most the window depth per step

TheoremThe idle-extended step is the situation step applied to the stacks#✓fully proved

Let \(M\) be a finite TM2 machine and \(c\) a configuration with label \(l\), state \(v\) and stacks \(S\), and let \((l', v', P, n)\) be the situation step of \(M\) at label \(l\) and state \(v\) on the windows of \(c\). Then the idle-extended step of \(M\) at \(c\) is the configuration with label \(l'\), state \(v'\) and, on each stack \(k\), the list \(P_k\) placed on top of what remains of \(S_k\) after removing its top \(n_k\) symbols.

This is an equality of full configurations and needs no bound on the stack heights.

theorem step_agree (M : FinTM2) (c : M.Cfg) :
    stepI M c = applyEff c.stk (sitStep M c.l c.var (winC M c))

Uses 9 · Used by 3

Statement usesApplying an effect to the original stacks · The situation step · Idle-extended step · Windows of a configuration

Proof usesWindow depth of a machine · Symbolic effect of a statement tree · The symbolic effect of a statement agrees with the real step · Stack operations on a path of a statement tree · Top window of a stack

Used byThe idle-extended step preserves good configurations · The table-driven step · Stack heights grow by at most the window depth per step

DefinitionLabel-and-state code of a configuration#✓fully proved

For an encoding \(E\) of a machine \(M\) and a configuration \(c\) of \(M\), this is the number that \(E\)'s (label, state) numbering assigns to the pair formed by the label of \(c\) (possibly the halted label) and the state of \(c\).

def code (c : M.Cfg) : ℕ := E.lc (c.l, c.var)

Uses 1 · Used by 30

Statement usesEncoding data for a finite TM2 machine

Used bySituation index of a configuration · The situation index matches the code and windows · The table-driven step · The table-driven step along a run · C1a (decoding recovers a good configuration) · 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) · Positive core of the 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 · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · L2 (S-definition, positive) · Update forcing (positive) · Update forcing, real run · Init semantics · Satisfying assignments yield accepting runs · Completeness of the accept family · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · Row-0 cells of the start configuration are run literals · The real run's literals · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · Situation injectivity · The run assignment satisfies the update family

DefinitionCell code of a configuration#✓fully proved

For an encoding \(E\) of a machine \(M\), a configuration \(c\) of \(M\) and natural numbers \(k\) and \(j\), this is the code under \(E\) of the symbol at position \(j\) (counting from \(0\) at the top) of the stack that \(E\)'s inverse stack numbering assigns to \(k\), in \(c\); it is \(0\) (the code of ⊥) if that stack has at most \(j\) symbols.

def cell (c : M.Cfg) (k j : ℕ) : ℕ := ((c.stk (E.kd k))[j]?).elim 0 (E.enc (E.kd k))

Uses 1 · Used by 41

Statement usesEncoding data for a finite TM2 machine

Used bySituation index of a configuration · The situation index matches the code and windows · The table-driven step · The table-driven step along a run · C1c (cell arrays of good configurations are well-formed rows) · C1a (decoding recovers a good configuration) · 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) · 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⁺) · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · 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 · 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 · Completeness of the accept family · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · Row-0 cells of the start configuration are run literals · The real run's literals · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · Situation injectivity · The run assignment satisfies the update family

DefinitionSituation index of a configuration#✓fully proved

Fix an encoding \(E\) of a finite TM2 machine \(M\), with \(K\) stacks, symbol-code bound \(g\) and window depth \(d\). The situation index of a configuration \(c\) is the number

\[\sum_{k < K} \sum_{j < d} \mathrm{cell}_c(k, j)\, g^{kd + j} + \mathrm{code}(c)\, g^{Kd},\]

where \(\mathrm{code}(c)\) is the combined (label, state) code of \(c\) and \(\mathrm{cell}_c(k, j)\) is the cell code of \(c\) on stack number \(k\) at depth \(j\) (\(0\) for the empty cell).

def sitIdx (c : M.Cfg) : ℕ :=
  mix E.g (E.code c) (E.KK * depth M) fun n => E.cell c (n / depth M) (n % depth M)

Uses 6 · Used by 27

Statement usesEncoding data for a finite TM2 machine · Cell code of a configuration · Label-and-state code of a configuration · Symbol-code bound · Mixed-radix number · Window depth of a machine

Used byThe situation index matches the code and windows · The table-driven step · The table-driven step along a run · C2' (decoding the table-driven row gives the next configuration) · 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⁺) · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · 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 · Completeness of the accept family · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · Row-0 cells of the start configuration are run literals · The real run's literals · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · Situation injectivity · The run assignment satisfies the update family

DefinitionThe table-driven row update#✓fully proved

Fix an encoding \(E\) of a finite TM2 machine, a row height \(H\), a situation \(i\) and an old row \(\mathrm{old}\) giving a code for each stack number \(k\) and depth \(j\). For a stack number \(k\), write \(p\) for the number of symbols situation \(i\) leaves pushed on stack \(k\) and \(n\) for the number of original symbols it consumes from stack \(k\). The updated row at \((k, j)\) is the code of the symbol situation \(i\) leaves at depth \(j\) of stack \(k\) if \(j < p\); otherwise it is \(\mathrm{old}(k, j - p + n)\) if \(j < (H \mathbin{\dot{-}} \max(p, n)) + p\), where \(\dot{-}\) is truncated subtraction; otherwise it is \(0\), the empty cell.

These are the three cases the shift clauses force: pushed fill, in-range shift and overflow.

def tabRow (H i : ℕ) (old : ℕ → ℕ → ℕ) (k j : ℕ) : ℕ :=
  if j < E.pl i k then E.pu i k j
  else if j < H - max (E.pl i k) (E.cn i k) + E.pl i k then old k (j - E.pl i k + E.cn i k)
  else 0

Uses 4 · Used by 14

Statement usesEncoding data for a finite TM2 machine · Consumption table of a situation · Push-count table of a situation · Pushed-symbol table of a situation

Used byThe table-driven step · The table-driven step along a run · C2' (decoding the table-driven row gives the next configuration) · 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⁺) · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · Update forcing, real run · The run assignment satisfies the cell-shift family · The run assignment satisfies the update family

DefinitionGood configurations#✓fully proved

For an encoding \(E\) of a machine \(M\), a configuration \(c\) of \(M\) is good when every symbol on every stack \(k\) of \(c\) is one of the effective symbols of stack \(k\) listed by \(E\) (so that it has a code).

def Good (c : M.Cfg) : Prop := ∀ k, ∀ x ∈ c.stk k, ∃ n, E.dec k n = x

Uses 1 · Used by 27

Statement usesEncoding data for a finite TM2 machine

Used byThe idle-extended step preserves good configurations · The situation index matches the code and windows · The table-driven step · The table-driven step along a run · C1c (cell arrays of good configurations are well-formed rows) · C1a (decoding recovers a good configuration) · C1d (decoded configurations are good) · C2' (decoding the table-driven row gives the next configuration) · Good configurations are determined by their row (C1f) · 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⁺) · Overflow cells of the next row hold the table value · Overflow cells of the next row on a real run · Pushed-fill forcing for a good configuration · Pushed-fill forcing on a real run · L2 (S-definition, positive) · L3 (S-definition, real run) · Update forcing (positive) · Update forcing, real run · Satisfying assignments yield accepting runs · Completeness of the accept family · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · The run assignment satisfies the cell-shift family · Situation injectivity

TheoremThe situation index matches the code and windows#✓fully proved

Fix an encoding \(E\) of a finite TM2 machine \(M\), with \(K\) stacks, \(N\) situations and window depth \(d\). If every symbol on every stack of a configuration \(c\) lies in the effective alphabet of \(E\), then the situation index \(i\) of \(c\) satisfies \(i < N\), the label/state code of situation \(i\) equals the combined (label, state) code of \(c\), and for all \(k < K\) and \(j < d\) the window symbol code of situation \(i\) on stack \(k\) at depth \(j\) equals the cell code of \(c\) on stack number \(k\) at depth \(j\).

theorem sitIdx_spec (c : M.Cfg) (hc : E.Good c) :
    E.sitIdx c < E.N ∧ E.la (E.sitIdx c) = E.code c ∧
      ∀ k < E.KK, ∀ j < depth M, E.wa (E.sitIdx c) k j = E.cell c k j

Uses 12 · Used by 12

Statement usesEncoding data for a finite TM2 machine · Good configurations · Number of situations · Cell code of a configuration · Label-and-state code of a configuration · Label/state code of a situation · Situation index of a configuration · Window symbol code of a situation · Window depth of a machine

Proof usesSymbol-code bound · The symbol-code bound is positive · Mixed-radix index of a situation

Used byThe table-driven step · The table-driven step along a run · Positive core of the shift step (L2⁺) · Overflow cells of the next row hold the table value · Pushed-fill forcing for a good configuration · L2 (S-definition, positive) · Update forcing (positive) · Completeness of the accept family · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · The run assignment satisfies the cell-shift family · Situation injectivity

TheoremCells of a pushed prefix over a truncated stack#✓fully proved

Let \(e\) map elements of \(\alpha\) to natural numbers, and for a list \(L\) over \(\alpha\) and \(i \in \mathbb{N}\) let \(L\langle i\rangle\) be \(e\) of the entry of \(L\) at position \(i\) (counting from \(0\)), or \(0\) if \(L\) has at most \(i\) entries. Subtraction of natural numbers is truncated at \(0\). Let \(P\) and \(S\) be lists over \(\alpha\) and \(n, H, d, j \in \mathbb{N}\) with \(|P| \le d\), \(n \le d\) and \(|S| \le H - d\), and let \(Q\) be \(P\) followed by \(S\) with its first \(n\) entries removed. If \(j < |P|\) then \(Q\langle j\rangle = P\langle j\rangle\); otherwise, if \(j < (H - \max(|P|, n)) + |P|\) then \(Q\langle j\rangle = S\langle j - |P| + n\rangle\); and otherwise \(Q\langle j\rangle = 0\).

theorem row_cell {α : Type} (e : α → ℕ) (P S : List α) (n H d j : ℕ) (hP : P.length ≤ d)
    (hn : n ≤ d) (hS : S.length ≤ H - d) :
    ((P ++ S.drop n)[j]?).elim 0 e =
      if j < P.length then (P[j]?).elim 0 e
      else if j < H - max P.length n + P.length then (S[j - P.length + n]?).elim 0 e
      else 0

Used by 1

Used byThe table-driven step

TheoremThe table-driven step#✓fully proved

Fix an encoding \(E\) of a finite TM2 machine \(M\), with \(K\) stacks and window depth \(d\), and a natural number \(H\). Let \(c\) be a configuration such that every symbol on every stack of \(c\) lies in the effective alphabet of \(E\) and every stack of \(c\) has length at most \(H \mathbin{\dot{-}} d\) (truncated subtraction). Let \(c'\) be the idle-extended step of \(M\) at \(c\) and \(i\) the situation index of \(c\). Then the combined (label, state) code of \(c'\) is the next label/state code after situation \(i\), and for all \(k < K\) and \(j < H\) the cell code of \(c'\) on stack number \(k\) at depth \(j\) is the value at \((k, j)\) of the table-driven row update with height \(H\) and situation \(i\) applied to the cell codes of \(c\).

No hypothesis \(d \le H\) is needed: if \(H < d\), every stack of \(c\) is empty.

theorem table_agree (H : ℕ) (c : M.Cfg) (hc : E.Good c)
    (hh : ∀ k, (c.stk k).length ≤ H - depth M) :
    E.code (stepI M c) = E.na (E.sitIdx c) ∧
      ∀ k < E.KK, ∀ j < H, E.cell (stepI M c) k j = E.tabRow H (E.sitIdx c) (E.cell c) k j

Uses 28 · 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 · 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 usesNumber of situations · Consumption table of a situation · Decoding a symbol code · Label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Effect of a situation · Cells of a pushed prefix over a truncated stack · The situation index matches the code and windows · Window symbol code of a situation · Decoded windows of a situation · Applying 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 · Top window of a stack

Used byThe table-driven step along a run · C2' (decoding the table-driven row gives the next configuration)

TheoremReads of the in-range shift stay in the row#✓fully proved

Fix an encoding \(E\) of a finite TM2 machine and natural numbers \(H\), \(i\), \(k\) and \(j\). Write \(p\) for the number of symbols situation \(i\) leaves pushed on stack number \(k\) and \(n\) for the number of original symbols it consumes from stack number \(k\). If \(p \le j\) and \(j < (H \mathbin{\dot{-}} \max(p, n)) + p\), where \(\dot{-}\) is truncated subtraction, then \(j - p + n < H\).

So every old cell that the table-driven row update reads lies in the row of height \(H\).

theorem tabRow_reads_lt (H i k j : ℕ) (hpl : E.pl i k ≤ j)
    (hj : j < H - max (E.pl i k) (E.cn i k) + E.pl i k) :
    j - E.pl i k + E.cn i k < H

Uses 3

Statement usesEncoding data for a finite TM2 machine · Consumption table of a situation · Push-count table of a situation

TheoremThe idle-extended step preserves good configurations#✓fully proved

Let \(E\) be an encoding of a finite TM2 machine \(M\) and let \(c\) be a configuration of \(M\). If \(c\) is good for \(E\), then so is the idle-extended step of \(M\) at \(c\).

theorem good_step (c : M.Cfg) (hc : E.Good c) : E.Good (stepI M c)

Uses 10 · Used by 13

Statement usesEncoding data for a finite TM2 machine · Good configurations · Idle-extended step

Proof usesSymbols a statement tree can push · Applying an effect to the original stacks · Symbolic effect of a statement tree · Pushed symbols come from the start or from push nodes · The situation step · The idle-extended step is the situation step applied to the stacks · Windows of a configuration

Used byThe table-driven step along a run · C2' (decoding the table-driven row gives the next configuration) · Exact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · Overflow cells of the next row on a real run · Pushed-fill forcing on a real run · L3 (S-definition, real run) · Update forcing, real run · Satisfying assignments yield accepting runs · Completeness of the accept family · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · The run assignment satisfies the cell-shift family

TheoremThe table-driven step along a run#✓fully proved

Fix an encoding \(E\) of a finite TM2 machine \(M\), with \(K\) stacks, \(N\) situations and window depth \(d\), a natural number \(H\), an input list \(s\) and a time \(t\). For each time \(u\) let \(c_u\) be the configuration at time \(u\) of the idle-extended run of \(M\) from the initial configuration of \(M\) on input \(s\), and let \(i\) be the situation index of \(c_t\). If every stack of \(c_t\) has length at most \(H \mathbin{\dot{-}} d\) (truncated subtraction), then \(i < N\); the label/state code of situation \(i\) is the combined (label, state) code of \(c_t\); for all \(k < K\) and \(j < d\) the window symbol code of situation \(i\) on stack \(k\) at depth \(j\) is the cell code of \(c_t\) on stack number \(k\) at depth \(j\); the combined (label, state) code of \(c_{t+1}\) is the next label/state code after situation \(i\); and for all \(k < K\) and \(j < H\) the cell code of \(c_{t+1}\) on stack number \(k\) at depth \(j\) is the value at \((k, j)\) of the table-driven row update with height \(H\) and situation \(i\) applied to the cell codes of \(c_t\).

Unlike the single-step version, no alphabet hypothesis is needed: every symbol on a stack of such a run lies in the effective alphabet of \(E\).

theorem table_agree_run (H : ℕ) (s : List (M.Γ M.k₀)) (t : ℕ)
    (hh : ∀ k, ((runI M (initList M s) t).stk k).length ≤ H - depth M) :
    let c := runI M (initList M s) t
    E.sitIdx c < E.N ∧ E.la (E.sitIdx c) = E.code c ∧
      (∀ k < E.KK, ∀ j < depth M, E.wa (E.sitIdx c) k j = E.cell c k j) ∧
      E.code (runI M (initList M s) (t + 1)) = E.na (E.sitIdx c) ∧
      ∀ k < E.KK, ∀ j < H,
        E.cell (runI M (initList M s) (t + 1)) k j = E.tabRow H (E.sitIdx c) (E.cell c) k j

Uses 15 · Used by 7

Statement usesEncoding data for a finite TM2 machine · Number of situations · Cell code of a configuration · Label-and-state code of a configuration · Label/state code of a situation · Next label/state code of a situation · Situation index of a configuration · The table-driven row update · Window symbol code of a situation · Window depth of a machine · Idle-extended run

Proof usesGood configurations · The idle-extended step preserves good configurations · The situation index matches the code and windows · The table-driven step

Used byExact shift step on a real run (L3) · Positive shift step on a real run (L3⁺) · Overflow cells of the next row on a real run · Pushed-fill forcing on a real run · Update forcing, real run · The run assignment satisfies the cell-shift family · The run assignment satisfies the update family

DefinitionReading a list from a sequence of cells#✓fully proved

For \(f\) mapping each natural number to an element of \(\alpha\) or to ⊥, and \(j, m \in \mathbb{N}\), this is the list \([x_0, \dots, x_{r-1}]\) with \(f(j + i) = x_i\) for each \(i < r\), where \(r = m\) if none of \(f(j), \dots, f(j + m - 1)\) is ⊥, and otherwise \(r\) is the least \(i < m\) with \(f(j + i) = \bot\).

def decS (f : ℕ → Option α) : ℕ → ℕ → List α
  | _, 0 => []
  | j, m + 1 => match f j with
    | none => []
    | some x => x :: decS f (j + 1) m

Used by 7

Used byReading back a list from its cells · C1 decoder (decoding a row) · C1e (the row decoder reads only the window) · C1a (decoding recovers a good configuration) · C1d (decoded configurations are good) · C1b (decoding a well-formed row loses nothing) · Entries of a decoded stack on prefix-form input

TheoremReading back a list from its cells#✓fully proved

Let \(f\) map each natural number to an element of \(\alpha\) or to ⊥, let \(S\) be a list over \(\alpha\), and let \(j, m \in \mathbb{N}\). Suppose that for every \(i \in \mathbb{N}\), \(f(j + i)\) is the entry of \(S\) at position \(i\) (counting from \(0\)) when \(i\) is less than the length of \(S\), and ⊥ otherwise. If \(S\) has length at most \(m\), then reading \(f\) from position \(j\) for at most \(m\) positions, stopping at the first ⊥, gives \(S\).

theorem decS_of_list (f : ℕ → Option α) : ∀ (S : List α) (j m : ℕ),
    (∀ i, f (j + i) = S[i]?) → S.length ≤ m → decS f j m = S

Uses 1 · Used by 1

Statement usesReading a list from a sequence of cells

Used byC1a (decoding recovers a good configuration)

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.