The idle-extended run follows the real run to Completeness of the five clause families

TheoremThe idle-extended run follows the real run#✓fully proved

Let \(M\) be a finite stack machine, let \(n \in \mathbb{N}\), and let \(c, c'\) be configurations of \(M\). If iterating the step function of \(M\) \(n\) times as a partial function, starting from \(c\), yields \(c'\), then the idle-extended run of \(M\) from \(c\) is at \(c'\) after \(n\) steps.

theorem runI_of_iterate (M : FinTM2) : ∀ (n : ℕ) (c c' : M.Cfg),
    (flip bind (TM2.step M.m))^[n] (some c) = some c' → runI M c n = c'

Uses 3 · Used by 2

Statement usesIdle-extended run

Proof usesUnfolding the idle-extended run from the front · Idle-extended step

Used byThe reduction machine halts with the emitted formula · The idle-extended run stays at the halting configuration

TheoremA halted configuration is fixed by the idle-extended run#✓fully proved

Let \(M\) be a finite stack machine and \(c\) a configuration of \(M\) whose label is empty (that is, \(c\) has halted). Then for every \(t \in \mathbb{N}\), the idle-extended run of \(M\) from \(c\) is at \(c\) after \(t\) steps.

theorem runI_halted (M : FinTM2) (c : M.Cfg) (hc : c.l = none) : ∀ t, runI M c t = c

Uses 2 · Used by 1

Statement usesIdle-extended run

Proof usesIdle-extended step

Used byThe idle-extended run stays at the halting configuration

TheoremThe idle-extended run stays at the halting configuration#✓fully proved

Let \(M\) be a machine, \(s\) a word over its input alphabet and \(l'\) a list over its output alphabet. Suppose that \(M\), started in the initial configuration on \(s\), reaches the halting configuration with output \(l'\) (halted, in the initial state, with \(l'\) on the output stack and every other stack empty) in at most \(p\) steps. Then for every \(T \ge p\), the configuration reached after \(T\) steps of the idle-extended run of \(M\) from the initial configuration on \(s\) is that halting configuration.

theorem runI_haltList (M : FinTM2) (s : List (M.Γ M.k₀)) (l' : List (M.Γ M.k₁)) {p : ℕ}
    (h : TM2OutputsInTime M s (some l') p) {T : ℕ} (hT : p ≤ T) :
    runI M (initList M s) T = haltList M l'

Uses 4 · Used by 1

Statement usesIdle-extended run

Proof usesA halted configuration is fixed by the idle-extended run · The idle-extended run follows the real run · Idle-extended step

Used byThe verifier's run settles on its output

TheoremAcceptance of a halting configuration#✓fully proved

Let \(M\) be a machine, \(l'\) a list over its output alphabet and \(\mathrm{acc}\) an output symbol. The halting configuration with output \(l'\) (halted, in the initial state, with \(l'\) on the output stack and every other stack empty) is accepting for \(\mathrm{acc}\) if and only if \(l'\) is nonempty and its first element is \(\mathrm{acc}\).

theorem accepts_haltList (M : FinTM2) (l' : List (M.Γ M.k₁)) (acc : M.Γ M.k₁) :
    Accepts M (haltList M l') acc ↔ l'.head? = some acc

Uses 1 · Used by 1

Statement usesAccepting configuration

Used byCorrectness of the reduction

TheoremUniqueness of quotient and remainder#✓fully proved

Let \(W\), \(t\), \(t'\), \(r\) and \(r'\) be natural numbers with \(r < W\) and \(r' < W\). If \(tW + r = t'W + r'\), then \(t = t'\) and \(r = r'\).

theorem row_pos_inj {W t t' r r' : ℕ} (hr : r < W) (hr' : r' < W)
    (h : t * W + r = t' * W + r') : t = t' ∧ r = r'

Used by 4

Used byCompleteness 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

TheoremEqual low-order digits give equal residues#✓fully proved

Let \(b\), \(i\), \(i'\) and \(n\) be natural numbers. If \(\lfloor i / b^e \rfloor \bmod b = \lfloor i' / b^e \rfloor \bmod b\) for every \(e < n\), that is, \(i\) and \(i'\) have the same first \(n\) base-\(b\) digits, then \(i \bmod b^n = i' \bmod b^n\).

theorem mod_pow_eq_of_digits {b i i' : ℕ} : ∀ n, (∀ e < n, i / b ^ e % b = i' / b ^ e % b) →
    i % b ^ n = i' % b ^ n

Used by 1

Used bySituation injectivity

TheoremSituation injectivity#✓fully proved

Let \(M\) be a finite stack machine with encoding data \(E\), and write \(N\) for the number of situations of \(E\), \(K\) for the number of stacks of \(E\) and \(d\) for the window depth of \(M\). Let \(c\) be a configuration of \(M\) all of whose stack symbols lie in the effective alphabets of \(E\), and let \(i < N\). If the label/state code of situation \(i\) equals the (label, state) code of \(c\), and for every stack number \(k < K\) and every depth \(j < d\) the window code of situation \(i\) at stack \(k\), depth \(j\) equals the cell code of \(c\) at stack \(k\), depth \(j\), then \(i\) is the situation index of \(c\).

This is the converse of the fact that the situation index of such a \(c\) is below \(N\) and has the code and the windows of \(c\).

theorem sit_inj (c : M.Cfg) (hc : E.Good c) {i : ℕ} (hi : i < E.N) (hl : E.la i = E.code c)
    (hw : ∀ k < E.KK, ∀ j < depth M, E.wa i k j = E.cell c k j) : i = E.sitIdx c

Uses 14 · Used by 1

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 usesNumber of window combinations · Symbol-code bound · The symbol-code bound is positive · The situation index matches the code and windows · Equal low-order digits give equal residues

Used byTransition families with a run-literal head are satisfied by the run

DefinitionThe real run's literals#✓fully proved

Let \(M\) be a finite stack machine with encoding data \(E\), let \(s\) be an input of \(M\) and \(H \in \mathbb{N}\), and for \(t \in \mathbb{N}\) let \(c_t\) be the configuration after \(t\) steps of the idle-extended run of \(M\) from its start configuration on \(s\). Variable indices are those of the layout of \(E\) at height \(H\), \(K\) is the number of stacks of \(E\), and \(A_0\) is the number of (label, state) codes of \(E\). An index \(p\) is a run literal when, for some time \(t\), it is one of the following: the label/state variable at time \(t\) for the (label, state) code of \(c_t\); for some stack number \(k < K\) and depth \(j < H\), the cell variable at time \(t\) for stack \(k\), depth \(j\) and the cell code of \(c_t\) at stack \(k\), depth \(j\) (code \(0\), the empty cell, included); or the label/state variable at time \(t + 1\) for \(A_0 + i\), where \(i\) is the situation index of \(c_t\).

def RunLit (s : List (M.Γ M.k₀)) (H p : ℕ) : Prop :=
  ∃ t, p = E.layout.xIdx H t (E.code (runI M (initList M s) t)) ∨
    (∃ k < E.KK, ∃ j < H, p = E.layout.cIdx H t k j (E.cell (runI M (initList M s) t) k j)) ∨
    p = E.layout.xIdx H (t + 1) (E.sa (E.sitIdx (runI M (initList M s) t)))

Uses 9 · Used by 9

Statement usesIndex of a cell variable in the transition-family layout · Index of a label/state variable · Encoding data for a finite TM2 machine · Cell code of a configuration · Label-and-state code of a configuration · Clause layout of a machine encoding · Position of a situation's variable · Situation index of a configuration · Idle-extended run

Used byCompleteness 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 assignment of the real run's literals · Faithful clauses with a literal agreeing with the real run are satisfied · Unit clauses on run literals are satisfied · The run assignment satisfies the cell-shift family

DefinitionThe assignment of the real run's literals#✓fully proved

Let \(E\) be an encoding of the machine \(M\), let \(s\) be a word over the input alphabet, let \(T\) and \(H\) be natural numbers, and let \(V\) be the number of variables of the transition-clause formula for \(T\) and \(H\). The assignment is the list of \(V\) truth values whose entry \(p\), for each \(p < V\), is true exactly when \(p\) is one of the real run's literals of \(s\) at height \(H\).

noncomputable def runAsg (s : List (M.Γ M.k₀)) (T H : ℕ) : List Bool :=
  (List.range (E.layout.numVars T H)).map fun p => decide (E.RunLit s H p)

Uses 4 · Used by 10

Statement usesNumber of variables of the transition-clause formula · Encoding data for a finite TM2 machine · The real run's literals · Clause layout of a machine encoding

Used byCompleteness 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 · Faithful clauses with a literal agreeing with the real run are satisfied · Unit clauses on run literals are satisfied · 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

TheoremFaithful clauses with a literal agreeing with the real run are satisfied#✓fully proved

Let \(M\) be a finite stack machine with encoding data \(E\), let \(s\) be an input of \(M\), let \(T, H \in \mathbb{N}\), and let \(V\) be the number of variables of the layout of \(E\) for \(T\) and \(H\). Let \(\ell\) be a list of literals that is faithful for \(V\), and let \((p, b) \in \ell\) be a literal such that \(b\) is true exactly when \(p\) is a run literal of \(s\) at height \(H\). Then the dense clause over \(V\) variables built from \(\ell\) is satisfied by the run assignment of \(s\) for \(T\) and \(H\), which is true exactly on the run literals.

theorem sat_run {s : List (M.Γ M.k₀)} {T H : ℕ} {ls : List (ℕ × Bool)}
    (hf : Faithful (E.layout.numVars T H) ls) {p : ℕ} {b : Bool} (hp : (p, b) ∈ ls)
    (hb : b = true ↔ E.RunLit s H p) :
    clauseSat (Family.denseClause (E.layout.numVars T H) ls) (E.runAsg s T H)

Uses 9 · Used by 5

Statement usesNumber of variables of the transition-clause formula · Dense clause from a list of literals · Encoding data for a finite TM2 machine · The real run's literals · Clause layout of a machine encoding · The assignment of the real run's literals · Faithful literal list · Satisfaction of a dense clause

Proof usesExact clause semantics

Used byCompleteness of the accept family · Transition families with a run-literal head are satisfied by the run · Completeness of the init family · Unit clauses on run literals are satisfied · The run assignment satisfies the cell-shift family

TheoremSituation variables lie in the label/state block#✓fully proved

Let \(E\) be an encoding of a finite TM2 machine with \(N\) situations. For every natural number \(i < N\), the position of the variable of situation \(i\) is less than the label/state block size \(A\) of the clause layout of \(E\).

theorem sa_lt {i : ℕ} (hi : i < E.N) : E.sa i < E.layout.A

Uses 5 · Used by 4

Statement usesVariable layout of the transition clauses · Encoding data for a finite TM2 machine · Number of situations · Clause layout of a machine encoding · Position of a situation's variable

Used byCompleteness 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

TheoremTransition families with a run-literal head are satisfied by the run#✓fully proved

Let \(E\) be an encoding of the machine \(M\) with layout \(L\), \(N\) situations, label/state table \(\mathrm{la}\) and window table \(\mathrm{wa}\), let \(d\) be the window depth of \(M\), and let \(T, H \in \mathbb{N}\) with \(d \le H\). Write \(X[r, x]\) for the index of the label/state variable \(x\) of row \(r\) at height \(H\). Fix an input list \(s\), let \(c_t\) be the configuration after \(t\) steps of the idle-extended run of \(M\) from the initial configuration on \(s\), and let \(\nu : \mathbb{N} \to \mathbb{N}\) be a next-label table such that \(\mathrm{la}\), \(\nu\) and \(\mathrm{wa}\) are well formed for \(L\) at height \(H\) for every situation \(i < N\). Suppose that for every \(t < T\), with \(i_t\) the situation index of \(c_t\), the index \(X[t + 1, \nu(i_t)]\) is one of the real run's literals of \(s\) at height \(H\). Then the assignment of the real run's literals of \(s\) for \(T\) and \(H\) satisfies the transition clause family of \(L\) with the tables \(\mathrm{la}\), \(\nu\) and \(\mathrm{wa}\) for \(T\), \(H\) and \(N\).

In clause \((t, i)\) the head literal is true when \(i\) is the situation index of \(c_t\); otherwise the clause is satisfied by a body literal whose variable is false, by situation injectivity.

theorem fam_complete {T H : ℕ} (s : List (M.Γ M.k₀)) (nx : ℕ → ℕ)
    (hwf : ∀ i < E.N, Family.WF E.layout E.la nx E.wa H i) (hdH : depth M ≤ H)
    (hnx : ∀ t < T,
        E.RunLit s H (E.layout.xIdx H (t + 1) (nx (E.sitIdx (runI M (initList M s) t))))) :
    cnfSat (Family.family E.layout E.la nx E.wa T H E.N) (E.runAsg s T H)

Uses 42 · Used by 2

Statement usesIndex of a label/state variable · Well-formed situation tables for the transition clauses · The transition clause family · Encoding data for a finite TM2 machine · Number of situations · The real run's literals · Label/state code of a situation · Clause layout of a machine encoding · The assignment of the real run's literals · Situation index of a configuration · Window symbol code of a situation · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesIncreasing literal positions · Variable layout of the transition clauses · Index of a cell variable in the transition-family layout · Number of literals of a transition clause · Number of variables of the transition-clause formula · Variables per time step · Dense clause from a list of literals · Successor of a number with a non-maximal remainder · Increasing literal sequences · Position of a literal in a transition clause · Literals of a transition clause · Number of window combinations · Good configurations · Cell code of a configuration · Label-and-state code of a configuration · Symbol-code bound · The symbol-code bound is positive · The idle-extended step preserves good configurations · Position of a situation's variable · Situation variables lie in the label/state block · Faithful clauses with a literal agreeing with the real run are satisfied · The situation index matches the code and windows · Situation injectivity · Faithful literal list · Uniqueness of quotient and remainder · Dense CNF formula · Dense clause · Satisfaction of a dense clause

Used byThe run assignment satisfies the situation-definition family · The run assignment satisfies the update family

TheoremThe run assignment satisfies the update family#✓fully proved

Let \(M\) be a finite stack machine with encoding data \(E\), let \(N\) be the number of situations of \(E\), let \(s\) be an input of \(M\), and let \(T, H \in \mathbb{N}\) with \(d \le H\), where \(d\) is the window depth of \(M\). For \(t \in \mathbb{N}\) let \(c_t\) be the configuration after \(t\) steps of the idle-extended run of \(M\) from its start configuration on \(s\), and suppose that for every \(t < T\) every stack of \(c_t\) has length at most \(H - d\). Then the run assignment of \(s\) for \(T\) and \(H\) (true exactly on the run literals) satisfies the transition clause family of the layout of \(E\) at height \(H\), for times \(t < T\) and situations \(i < N\), with the tables \(\mathrm{la}\), \(\mathrm{na}\) and \(\mathrm{wa}\) of \(E\).

In the clause of the real situation, the head literal is the code of the real next configuration, by the agreement of the tables with the machine's step.

theorem upd_complete {T H : ℕ} (s : List (M.Γ M.k₀)) (hdH : depth M ≤ H)
    (hh : ∀ t < T, ∀ k, ((runI M (initList M s) t).stk k).length ≤ H - depth M) :
    cnfSat (Family.family E.layout E.la E.na E.wa T H E.N) (E.runAsg s T H)

Uses 21 · Used by 1

Statement usesThe transition clause family · Encoding data for a finite TM2 machine · Number of situations · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · The assignment of the real run's literals · Window symbol code of a situation · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesIndex of a cell variable in the transition-family layout · Index of a label/state variable · Cell code of a configuration · Label-and-state code of a configuration · Transition families with a run-literal head are satisfied by the run · Position of a situation's variable · Situation index of a configuration · The table-driven row update · The table-driven step along a run · The transition tables of a machine are well formed

Used byCompleteness of the five clause families

TheoremThe run assignment satisfies the situation-definition family#✓fully proved

Let \(M\) be a finite stack machine with encoding data \(E\), let \(N\) be the number of situations of \(E\), let \(s\) be an input of \(M\), and let \(T, H \in \mathbb{N}\) with \(d \le H\), where \(d\) is the window depth of \(M\). Then the run assignment of \(s\) for \(T\) and \(H\) (true exactly on the run literals) satisfies the transition clause family of the layout of \(E\) at height \(H\), for times \(t < T\) and situations \(i < N\), with the tables \(\mathrm{la}\) and \(\mathrm{wa}\) of \(E\) and with the situation positions \(\mathrm{sa}\) of \(E\) in place of the next-label table.

In the clause of the real situation, the head literal is the real situation literal, by the definition of the run literals.

theorem sdef_complete {T H : ℕ} (s : List (M.Γ M.k₀)) (hdH : depth M ≤ H) :
    cnfSat (Family.family E.layout E.la E.sa E.wa T H E.N) (E.runAsg s T H)

Uses 18 · Used by 1

Statement usesThe transition clause family · Encoding data for a finite TM2 machine · Number of situations · Label/state code of a situation · Clause layout of a machine encoding · The assignment of the real run's literals · Position of a situation's variable · Window symbol code of a situation · Window depth of a machine · Satisfaction of a dense CNF formula

Proof usesIndex of a cell variable in the transition-family layout · Index of a label/state variable · Cell code of a configuration · Label-and-state code of a configuration · Transition families with a run-literal head are satisfied by the run · Situation index of a configuration · The situation-definition tables of a machine are well formed · Idle-extended run

Used byCompleteness of the five clause families

TheoremThe run assignment satisfies the cell-shift family#✓fully proved

Let \(M\) be a finite stack machine with encoding data \(E\), let \(N\) be the number of situations of \(E\), let \(s\) be an input of \(M\), and let \(T, H \in \mathbb{N}\) with \(d \le H\), where \(d\) is the window depth of \(M\). For \(t \in \mathbb{N}\) let \(c_t\) be the configuration after \(t\) steps of the idle-extended run of \(M\) from its start configuration on \(s\), and suppose that for every \(t < T\) every stack of \(c_t\) has length at most \(H - d\). Then the run assignment of \(s\) for \(T\) and \(H\) (true exactly on the run literals) satisfies the cell-shift clause family (shift, overflow and pushed-fill clauses) of the layout of \(E\) with the tables \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\) of \(E\), for \(N\) situations, times \(t < T\) and height \(H\).

Off the real situation the negated situation literal is true; on it, the target cell of row \(t + 1\) is the one given by the table-driven row update.

theorem shift_complete {T H : ℕ} (s : List (M.Γ M.k₀)) (hdH : depth M ≤ H)
    (hh : ∀ t < T, ∀ k, ((runI M (initList M s) t).stk k).length ≤ H - depth M) :
    cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T H) (E.runAsg s T H)

Uses 64 · Used by 1

Statement usesThe cell-shift clause family · Encoding data for a finite TM2 machine · Number of situations · Consumption table of a situation · Clause layout of a machine encoding · Push-count table of a situation · Pushed-symbol table of a situation · The assignment of the real run's literals · Position of a situation's variable · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesIncreasing literal positions · Variable layout of the transition clauses · Index of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Variables per time step · Index of a label/state variable · Dense clause from a list of literals · Increasing literal sequences · Clause kinds of the cell-shift family · Number of literals of a cell-shift clause kind · Literal signs of a shift clause kind · Increasing literal positions below a bound · Well-formed situation tables for the cell-shift family · Boundary before a literal · Literals of a clause kind at given positions · Literals of an overflow clause · Literal positions of an overflow clause · Literals of a pushed-fill clause · Literal positions of a pushed-fill clause · The shift block of a situation and a stack · Literals of an in-range shift clause · Literal positions of an in-range shift clause · Good configurations · The real run's literals · Cell code of a configuration · Label-and-state code of a configuration · Decoding a symbol code · Symbol-code bound · The symbol-code bound is positive · The idle-extended step preserves good configurations · Label/state code of a situation · Next label/state code of a situation · Pushed codes are valid symbol codes · Effect of a situation · Situation variables lie in the label/state block · Faithful clauses with a literal agreeing with the real run are satisfied · Situation index of a configuration · The situation index matches the code and windows · The table-driven row update · The table-driven step along a run · Window symbol code of a situation · The cell-shift tables of a machine are well formed · Decoded windows of a situation · Faithful literal list · 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 · Uniqueness of quotient and remainder · The situation step · Dense CNF formula · Dense clause · Satisfaction of a dense clause

Used byCompleteness of the five clause families

TheoremUnit clauses on run literals are satisfied#✓fully proved

Let \(M\) be a finite stack machine with encoding data \(E\), let \(s\) be an input of \(M\), let \(T, H \in \mathbb{N}\), and let \(V\) be the number of variables of the layout of \(E\) for \(T\) and \(H\). If \(p < V\) is a run literal of \(s\) at height \(H\), then the dense clause over \(V\) variables whose only literal is \(x_p\) is satisfied by the run assignment of \(s\) for \(T\) and \(H\), which is true exactly on the run literals.

theorem sat_unit {s : List (M.Γ M.k₀)} {T H p : ℕ} (hp : p < E.layout.numVars T H)
    (h : E.RunLit s H p) :
    clauseSat (Family.denseClause (E.layout.numVars T H) [(p, true)]) (E.runAsg s T H)

Uses 9 · Used by 1

Statement usesNumber of variables of the transition-clause formula · Dense clause from a list of literals · Encoding data for a finite TM2 machine · The real run's literals · Clause layout of a machine encoding · The assignment of the real run's literals · Satisfaction of a dense clause

Proof usesFaithful clauses with a literal agreeing with the real run are satisfied · Faithful literal list

Used byCompleteness of the init family

TheoremRow-0 cells of the start configuration are run literals#✓fully proved

Let \(E\) be an encoding of the machine \(M\) with \(K\) stacks, let \(s\) be a word over the input alphabet, and let \(H\), \(k\) and \(j\) be natural numbers with \(k < K\) and \(j < H\). Let \(x\) be the code of the cell of stack \(k\) at depth \(j\) in the initial configuration on \(s\). Then the cell variable of time \(0\), stack \(k\), depth \(j\) and symbol code \(x\) at height \(H\) is one of the real run's literals of \(s\) at height \(H\).

theorem lit_cell0 (s : List (M.Γ M.k₀)) {H k j : ℕ} (hk : k < E.KK) (hj : j < H) :
    E.RunLit s H (E.layout.cIdx H 0 k j (E.cell (initList M s) k j))

Uses 10 · Used by 1

Statement usesIndex of a cell variable in the transition-family layout · Encoding data for a finite TM2 machine · The real run's literals · Cell code of a configuration · Clause layout of a machine encoding

Proof usesIndex of a label/state variable · Label-and-state code of a configuration · Position of a situation's variable · Situation index of a configuration · Idle-extended run

Used byCompleteness of the init family

TheoremCompleteness of the init family#✓fully proved

Let \(E\) be an encoding of the machine \(M\), let \(x\), \(y\) and \(Y\) be words over the input alphabet such that every letter of \(y\) occurs in \(Y\), and let \(m\), \(T\) and \(H\) be natural numbers with \(|xy| \le m < H\), where \(xy\) is the concatenation. Then the assignment of the real run's literals of \(xy\) for \(T\) steps at height \(H\) satisfies the init family (clauses I1 to I6) for \(x\), \(Y\), \(m\), \(T\) and \(H\).

theorem init_complete {x y Ys : List (M.Γ M.k₀)} {m T H : ℕ} (hy : ∀ z ∈ y, z ∈ Ys)
    (hl : (x ++ y).length ≤ m) (hmH : m < H) :
    cnfSat (E.initFamily x Ys m T H) (E.runAsg (x ++ y) T H)

Uses 45 · Used by 1

Statement usesEncoding data for a finite TM2 machine · The row-0 init family of an encoding · The assignment of the real run's literals · Satisfaction of a dense CNF formula

Proof usesIncreasing literal positions · Variable layout of the transition clauses · Index of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Variables per time step · Index of a label/state variable · Dense clause from a list of literals · Good configurations · Number of situations · The real run's literals · Cell code of a configuration · Label-and-state code of a configuration · Symbol-code bound · The symbol-code bound is positive · The idle-extended step preserves good configurations · Certificate clauses of the init family · Start-code clause of the init family · Input clauses of the init family · Empty-stack clauses of the init family · Prefix clauses of the init family · Length-bound clauses of the init family · Label/state code of a situation · Clause layout of a machine encoding · Row-0 cells of the start configuration are run literals · Position of a situation's variable · Situation variables lie in the label/state block · Faithful clauses with a literal agreeing with the real run are satisfied · Unit clauses on run literals are satisfied · Situation index of a configuration · The situation index matches the code and windows · Window symbol code of a situation · Index of the empty-cell variable of the input stack · Faithful literal list · Satisfying a concatenation of CNF formulas · Window depth of a machine · Variables of rows up to the time bound · Uniqueness of quotient and remainder · Idle-extended run · Dense CNF formula · Dense clause · Satisfaction of a dense clause

Used byCompleteness of the five clause families

TheoremCompleteness of the accept family#✓fully proved

Let \(E\) be an encoding of the machine \(M\), let \(s\) be a word over the input alphabet, let \(T\) and \(H\) be natural numbers with \(H > 0\), and let \(\mathrm{acc}\) be a symbol of the output stack. Suppose that the configuration reached after \(T\) steps of the idle-extended run of \(M\) from the initial configuration on \(s\) is accepting for \(\mathrm{acc}\): it is halted, its state is the initial state of \(M\), and \(\mathrm{acc}\) is on top of its output stack. Then the assignment of the real run's literals of \(s\) for \(T\) steps at height \(H\) satisfies the accept family for \(\mathrm{acc}\) at \(T\) and \(H\), both its positive and its negated unit clauses.

theorem acc_complete (s : List (M.Γ M.k₀)) {T H : ℕ} {acc : M.Γ M.k₁} (hH : 0 < H)
    (hA : Accepts M (runI M (initList M s) T) acc) :
    cnfSat (E.accFamily acc T H) (E.runAsg s T H)

Uses 38 · Used by 1

Statement usesAccepting configuration · Encoding data for a finite TM2 machine · The accept family · The assignment of the real run's literals · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Number of variables of the transition-clause formula · Variables per time step · Index of a label/state variable · Dense clause from a list of literals · Good configurations · Number of situations · The real run's literals · Accept-cell clauses · Accept-code clauses · Accepting code · Cell code of a configuration · Label-and-state code of a configuration · Symbol-code bound · The symbol-code bound is positive · The idle-extended step preserves good configurations · Label/state code of a situation · Clause layout of a machine encoding · Position of a situation's variable · Situation variables lie in the label/state block · Faithful clauses with a literal agreeing with the real run are satisfied · Situation index of a configuration · The situation index matches the code and windows · Window symbol code of a situation · Faithful literal list · Window depth of a machine · Variables of rows up to the time bound · Uniqueness of quotient and remainder · Dense CNF formula · Dense clause · Satisfaction of a dense clause

Used byCompleteness of the five clause families

TheoremCompleteness of the five clause families#✓fully proved

Let \(E\) be an encoding of the machine \(M\), let \(x\), \(y\) and \(Y\) be words over the input alphabet such that every letter of \(y\) occurs in \(Y\), and let \(m\) and \(T\) be natural numbers with \(|xy| \le m\), where \(xy\) is the concatenation. Let \(d\) be the window depth of \(M\), let \(H = m + (T + 1)d + 1\) be the stack cap, and let \(a\) be the assignment of the real run's literals of \(xy\) for \(T\) steps at height \(H\). Suppose that the configuration reached after \(T\) steps of the idle-extended run of \(M\) from the initial configuration on \(xy\) is accepting for the output symbol \(\mathrm{acc}\): it is halted, its state is the initial state of \(M\), and \(\mathrm{acc}\) is on top of its output stack. Then the length of \(a\) is the number of variables of the transition-clause formula for \(T\) and \(H\), and \(a\) satisfies each of the following, all for \(T\) steps at height \(H\): the update family (the transition clause family with tables \(\mathrm{la}\), \(\mathrm{na}\), \(\mathrm{wa}\) and \(N\) situations), the S-definition family (the transition clause family with tables \(\mathrm{la}\), \(\mathrm{sa}\), \(\mathrm{wa}\) and \(N\) situations), the cell-shift family with tables \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\) and \(N\) situations, the init family for \(x\), \(Y\) and \(m\), and the accept family for \(\mathrm{acc}\).

No bound \(|x| \le m\) and no encodability of \(\mathrm{acc}\) is needed in this direction.

theorem accept_complete {x y Ys : List (M.Γ M.k₀)} {m T : ℕ} {acc : M.Γ M.k₁}
    (hy : ∀ z ∈ y, z ∈ Ys) (hl : (x ++ y).length ≤ m)
    (hA : Accepts M (runI M (initList M (x ++ y)) T) acc) :
    let a := E.runAsg (x ++ y) T (capH m T (depth M))
    a.length = E.layout.numVars T (capH m T (depth M)) ∧
    cnfSat (Family.family E.layout E.la E.na E.wa T (capH m T (depth M)) E.N) a ∧
    cnfSat (Family.family E.layout E.la E.sa E.wa T (capH m T (depth M)) E.N) a ∧
    cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T (capH m T (depth M))) a ∧
    cnfSat (E.initFamily x Ys m T (capH m T (depth M))) a ∧
    cnfSat (E.accFamily acc T (capH m T (depth M))) a

Uses 28 · Used by 1

Statement usesNumber of variables of the transition-clause formula · The transition clause family · The cell-shift clause family · Accepting configuration · Encoding data for a finite TM2 machine · Number of situations · The accept family · Consumption table of a situation · The row-0 init family of an encoding · Label/state code of a situation · Clause layout of a machine encoding · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · The assignment of the real run's literals · Position of a situation's variable · Window symbol code of a situation · Stack cap · Window depth of a machine · Idle-extended run · Satisfaction of a dense CNF formula

Proof usesThe real run's literals · Completeness of the accept family · Completeness of the init family · The run assignment satisfies the situation-definition family · The run assignment satisfies the cell-shift family · The run assignment satisfies the update family · Stack heights are at most the cap minus the window depth

Used byThe five Cook–Levin clause families are satisfiable iff some certificate is accepted

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.