A satisfying assignment tracks a certified run to Unfolding the idle-extended run from the front

TheoremA satisfying assignment tracks a certified run#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with window depth \(d\), let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), let \(m, T \in \mathbb{N}\) with \(|x| \le m\), and let \(H = m + (T + 1)d + 1\) be the corrected stack cap. Write \(\mathrm{la}, \mathrm{na}, \mathrm{sa}, \mathrm{wa}, \mathrm{pl}, \mathrm{cn}, \mathrm{pu}\) for the situation tables of \(E\) and \(N\) for its number of situations. Suppose an assignment \(a\) satisfies the following families at bounds \(T\) and \(H\): the transition clause family of the layout of \(E\) for \(N\) situations with tables \(\mathrm{la}\), \(\mathrm{na}\), \(\mathrm{wa}\) (the update family); the transition clause family for \(N\) situations with tables \(\mathrm{la}\), \(\mathrm{sa}\), \(\mathrm{wa}\) (the S-definition family); the cell-shift clause family for \(N\) situations with tables \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\); and the init family of \(E\) for \(x\), \(Y\), \(m\). Then there is a list \(y\) of symbols, each in \(Y\), with \(|xy| \le m\) such that for every \(t \le T\), if \(c_t\) is the configuration after \(t\) steps of the idle-extended run of \(M\) from the initial configuration on input \(xy\), then under \(a\) the variable of row \(t\) for the (label, state) code of \(c_t\) is true, and for every stack number \(k\) of \(E\) and every depth \(j < H\) the variable of row \(t\) for stack \(k\), depth \(j\) and the cell code of \(c_t\) at \((k, j)\) is true.

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

Uses 22 · Used by 1

Statement usesThe transition clause family · The cell-shift clause family · Encoding data for a finite TM2 machine · Cell literals of an array hold in a row · The code of a configuration holds in a row · Number of situations · Cell code of a configuration · 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 · 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 init family discharges the init obligation · Run tracking from the init obligation

Used bySatisfying assignments yield accepting runs

DefinitionFaithful literal list#✓fully proved

A list \(\ell\) of literals \((p, b)\), each a variable index \(p \in \mathbb{N}\) with a sign \(b\), is faithful for \(V \in \mathbb{N}\) when every literal \((p, b)\) of \(\ell\) has \(p < V\) and the first literal of \(\ell\) with index \(p\) is \((p, b)\).

Equivalently, every literal of \(\ell\) survives into the dense clause over \(V\) variables built from \(\ell\): it is in range, and not shadowed by an earlier literal at the same index with the other sign.

def Faithful (V : ℕ) (ls : List (ℕ × Bool)) : Prop :=
  ∀ p b, (p, b) ∈ ls → p < V ∧ ls.lookup p = some b

Used by 12

Used byExact clause semantics · Faithful dense clause family · Faithful dense clause family with positive literals · The init family is faithful with positive literals · The all-true assignment satisfies a faithful clause with a positive literal · The all-true assignment satisfies the transition, shift and init families · Completeness of the accept family · 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 cell-shift family

DefinitionFaithful dense clause family#✓fully proved

A CNF formula \(\varphi\) is a faithful family over \(V\) variables when every clause of \(\varphi\) is the dense clause over \(V\) variables built from some list of literals that is faithful for \(V\).

def FamOK (V : ℕ) (φ : CNF) : Prop :=
  ∀ c ∈ φ, ∃ ls, c = Family.denseClause V ls ∧ Faithful V ls

Uses 4

Statement usesDense clause from a list of literals · Faithful literal list · Dense CNF formula · Dense clause

DefinitionFaithful dense clause family with positive literals#✓fully proved

A CNF formula \(\varphi\) is a faithful family with positive literals over \(V\) variables when every clause of \(\varphi\) is the dense clause over \(V\) variables built from some list \(\ell\) of literals that is faithful for \(V\) and contains a positive literal \((p, \mathrm{true})\) for some \(p\).

def FamPos (V : ℕ) (φ : CNF) : Prop :=
  ∀ c ∈ φ, ∃ ls, c = Family.denseClause V ls ∧ Faithful V ls ∧ ∃ p, (p, true) ∈ ls

Uses 4 · Used by 2

Statement usesDense clause from a list of literals · Faithful literal list · Dense CNF formula · Dense clause

Used byThe init family is faithful with positive literals · The all-true assignment satisfies the transition, shift and init families

TheoremExact clause semantics#✓fully proved

Let \(V \in \mathbb{N}\), let \(\ell\) be a list of pairs \((p, b)\) of a variable index \(p\) and a sign \(b\) that is faithful for \(V\), and let \(a\) be a list of Booleans. Then \(a\) satisfies the dense clause over \(V\) variables built from \(\ell\) if and only if some \((p, b) \in \ell\) has \(p < |a|\) and \(a_p = b\).

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

Uses 5 · Used by 2

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

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

Used byThe all-true assignment satisfies a faithful clause with a positive literal · Faithful clauses with a literal agreeing with the real run are satisfied

TheoremThe all-true assignment satisfies a faithful clause with a positive literal#✓fully proved

Let \(V \in \mathbb{N}\) and let \(\ell\) be a list of literals that is faithful for \(V\) and contains a positive literal \((p, \mathrm{true})\). Then the all-true assignment of length \(V\) satisfies the dense clause over \(V\) variables built from \(\ell\).

theorem sat_allTrue {V : ℕ} {ls : List (ℕ × Bool)} (hf : Faithful V ls) (hp : ∃ p, (p, true) ∈ ls) :
    clauseSat (Family.denseClause V ls) (List.replicate V true)

Uses 4 · Used by 1

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

Proof usesExact clause semantics

Used byThe all-true assignment satisfies the transition, shift and init families

TheoremVariables of rows up to the time bound#✓fully proved

Let \(L\) be a layout, let \(T\), \(H\), \(t\) and \(p\) be natural numbers with \(t \le T\), and let \(W\) be the number of variables per time step of \(L\) at height \(H\). If \(p < (t + 1) W\), then \(p\) is less than the number of variables of \(L\) for bounds \(T\) and \(H\).

theorem lt_numVars {L : Family.Layout} {T H t p : ℕ} (ht : t ≤ T) (hp : p < (t + 1) * L.rowW H) :
    p < L.numVars T H

Uses 3 · Used by 4

Statement usesVariable layout of the transition clauses · Number of variables of the transition-clause formula · Variables per time step

Used byThe all-true assignment violates the accept family · The init family is faithful with positive literals · Completeness of the accept family · Completeness of the init family

TheoremThe init family is faithful with positive literals#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), and let \(m, T, H \in \mathbb{N}\) with \(|x| \le m < H\). Let \(V\) be the number of variables of the layout of \(E\) at bounds \(T\) and \(H\). Then every clause of the init family of \(E\) for \(x\), \(Y\), \(m\), \(T\), \(H\) is the dense clause over \(V\) variables built from a list of literals that is faithful for \(V\) and contains a positive literal; that is, the init family is a faithful family with positive literals over \(V\) variables.

theorem init_pos {x Ys : List (M.Γ M.k₀)} {m T H : ℕ} (hx : x.length ≤ m) (hmH : m < H) :
    FamPos (E.layout.numVars T H) (E.initFamily x Ys m T H)

Uses 25 · Used by 1

Statement usesNumber of variables of the transition-clause formula · Encoding data for a finite TM2 machine · The row-0 init family of an encoding · Clause layout of a machine encoding · Faithful dense clause family with positive literals

Proof usesIncreasing literal positions · Variable layout of the transition clauses · Index of a cell variable in the transition-family layout · Variables per time step · Index of a label/state variable · Dense clause from a list of literals · Number of situations · Symbol-code bound · The symbol-code bound is positive · 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 · Index of the empty-cell variable of the input stack · Faithful literal list · Variables of rows up to the time bound · Dense CNF formula · Dense clause

Used byThe all-true assignment satisfies the transition, shift and init families

DefinitionAccepting code#✓fully proved

For an encoding \(E\) of a finite stack machine \(M\), the accepting code is the (label, state) code that \(E\) assigns to the pair of the halted label and the initial state of \(M\), the label and state of a halted configuration as acceptance reads it.

def acode : ℕ := E.lc (none, M.initialState)

Uses 1 · Used by 10

Statement usesEncoding data for a finite TM2 machine

Used byThe concrete accept family is a layout-level accept family · Time bound of the accept generator for a concrete machine · Accept-code clauses · Accept-code clauses pin the (label, state) code · The all-true assignment violates the accept family · Satisfying assignments yield accepting runs · Completeness of the accept family · The host on the real generators of a machine · The assembled generator, after the precomputation · Every clause of the Cook–Levin formula has one slot per variable

DefinitionAccept-code clauses#✓fully proved

Let \(E\) be an encoding of a finite stack machine \(M\) with \(A_0\) (label, state) codes, let \(c^\ast\) be the code that \(E\) assigns to the halted label together with the initial state of \(M\), and let \(T, H \in \mathbb{N}\). In the layout of \(E\) at height \(H\), let \(W\) be the row width, \(V = (T + 1)W\) the number of variables, and \(X[t, u] = tW + u\) the label/state variable \(u\) at time \(t\). The accept-code clauses are the CNF formula listing, for each \(u < A_0\) in increasing order, the dense clause over \(V\) variables built from the single literal \(X[T, u]\) if \(u = c^\ast\) and \(\neg X[T, u]\) otherwise.

def accCode (T H : ℕ) : CNF :=
  (List.range E.A0).map fun u => Family.denseClause (E.layout.numVars T H)
    [(E.layout.xIdx H T u, decide (u = E.acode))]

Uses 8 · Used by 4

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

Used byAccept-cell clauses pin the top output symbol · Accept-code clauses pin the (label, state) code · The accept family · Completeness of the accept family

DefinitionAccept-cell clauses#✓fully proved

Let \(E\) be an encoding of a finite stack machine \(M\) with output stack \(k_1\), \(g\) symbol codes and stack numbering \(\kappa\), let \(\alpha\) be a symbol of stack \(k_1\) with code \(e\), and let \(T, H \in \mathbb{N}\). In the layout of \(E\) at height \(H\), let \(W\) be the row width, \(V = (T + 1)W\) the number of variables, and \(C[t, k, j, x]\) the variable for stack \(k\), depth \(j\) and symbol code \(x\) at time \(t\). The accept-cell clauses are the CNF formula listing, for each \(x < g\) in increasing order, the dense clause over \(V\) variables built from the single literal \(C[T, \kappa(k_1), 0, x]\) if \(x = e\) and \(\neg C[T, \kappa(k_1), 0, x]\) otherwise.

def accCell (acc : M.Γ M.k₁) (T H : ℕ) : CNF :=
  (List.range E.g).map fun x => Family.denseClause (E.layout.numVars T H)
    [(E.layout.cIdx H T (E.kc M.k₁) 0 x, decide (x = E.enc M.k₁ acc))]

Uses 8 · Used by 4

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

Used byAccept-cell clauses pin the top output symbol · Accept-code clauses pin the (label, state) code · The accept family · Completeness of the accept family

DefinitionThe accept family#✓fully proved

Let \(E\) be an encoding of a finite stack machine \(M\), let \(\alpha\) be a symbol of the output stack of \(M\), and let \(T, H \in \mathbb{N}\). The accept family for \(\alpha\) at bounds \(T\) and \(H\) is the CNF formula formed by the accept-code clauses at \(T\) and \(H\) followed by the accept-cell clauses for \(\alpha\) at \(T\) and \(H\).

def accFamily (acc : M.Γ M.k₁) (T H : ℕ) : CNF := E.accCode T H ++ E.accCell acc T H

Uses 5 · Used by 13

Statement usesEncoding data for a finite TM2 machine · Accept-cell clauses · Accept-code clauses · Dense CNF formula · Dense clause

Used byThe concrete accept family is a layout-level accept family · Time bound of the accept generator for a concrete machine · Accept-cell clauses pin the top output symbol · Accept-code clauses pin the (label, state) code · The all-true assignment violates the accept family · Satisfying assignments yield accepting runs · No accepting certificate, no satisfying assignment · Completeness of the accept family · Completeness of the five clause families · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · The formula emitted by the host · Correctness of the assembled formula · The assembled generator, after the precomputation

TheoremAccept-code clauses pin the (label, state) code#✓fully proved

Let \(E\) be an encoding of a finite stack machine \(M\) with \(A_0\) (label, state) codes, let \(\alpha\) be a symbol of the output stack of \(M\), and let \(T, H, u \in \mathbb{N}\) with \(u < A_0\). In the layout of \(E\) at height \(H\), let \(X[t, w]\) be the label/state variable \(w\) at time \(t\), and call a variable \(v\) true under an assignment \(a\) when \(v < |a|\) and \(a_v\) is true. If an assignment \(a\) satisfies the accept family for \(\alpha\) at bounds \(T\) and \(H\), and \(X[T, u]\) is true under \(a\), then \(u\) is the code that \(E\) assigns to the halted label together with the initial state of \(M\).

theorem acc_code {acc : M.Γ M.k₁} {T H u : ℕ} {a : List Bool} (h : cnfSat (E.accFamily acc T H) a)
    (hu : u < E.A0) (ht : Tr a (E.layout.xIdx H T u)) : u = E.acode

Uses 14 · Used by 2

Statement usesIndex of a label/state variable · Encoding data for a finite TM2 machine · The accept family · Accepting code · Clause layout of a machine encoding · 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 · Accept-cell clauses · Accept-code clauses · L0 (a satisfied dense clause has a satisfied listed literal) · Dense CNF formula · Dense clause

Used byThe all-true assignment violates the accept family · Satisfying assignments yield accepting runs

TheoremAccept-cell clauses pin the top output symbol#✓fully proved

Let \(E\) be an encoding of a finite stack machine \(M\) with output stack \(k_1\), \(g\) symbol codes and stack numbering \(\kappa\), let \(\alpha\) be a symbol of stack \(k_1\), and let \(T, H, x \in \mathbb{N}\) with \(x < g\). In the layout of \(E\) at height \(H\), let \(C[t, k, j, z]\) be the variable for stack \(k\), depth \(j\) and symbol code \(z\) at time \(t\), and call a variable \(v\) true under an assignment \(a\) when \(v < |a|\) and \(a_v\) is true. If an assignment \(a\) satisfies the accept family for \(\alpha\) at bounds \(T\) and \(H\), and the variable \(C[T, \kappa(k_1), 0, x]\) is true under \(a\), then \(x\) is the code of \(\alpha\) for stack \(k_1\).

theorem acc_cell {acc : M.Γ M.k₁} {T H x : ℕ} {a : List Bool} (h : cnfSat (E.accFamily acc T H) a)
    (hx : x < E.g) (ht : Tr a (E.layout.cIdx H T (E.kc M.k₁) 0 x)) : x = E.enc M.k₁ acc

Uses 14 · Used by 1

Statement usesIndex of a cell variable in the transition-family layout · Encoding data for a finite TM2 machine · The accept family · Symbol-code bound · Clause layout of a machine encoding · 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 · Accept-cell clauses · Accept-code clauses · L0 (a satisfied dense clause has a satisfied listed literal) · Dense CNF formula · Dense clause

Used bySatisfying assignments yield accepting runs

DefinitionAccepting configuration#✓fully proved

A configuration \(c\) of a finite stack machine \(M\) is accepting for a symbol \(\alpha\) of the output stack of \(M\) when \(c\) is halted (it has no label), its state is the initial state of \(M\), and the output stack of \(c\) is nonempty with top symbol \(\alpha\).

This is the shape of the halting configuration with output \([\alpha]\) that acceptance reads.

def Accepts (M : FinTM2) (c : M.Cfg) (acc : M.Γ M.k₁) : Prop :=
  c.l = none ∧ c.var = M.initialState ∧ (c.stk M.k₁).head? = some acc

Used by 8

Used byCorrectness of the reduction · Satisfying assignments yield accepting runs · No accepting certificate, no satisfying assignment · Completeness of the accept family · Completeness of the five clause families · Acceptance of a halting configuration · The five Cook–Levin clause families are satisfiable iff some certificate is accepted · Correctness of the assembled formula

TheoremSatisfying assignments yield accepting runs#✓fully proved

Let \(E\) be an encoding of a finite stack machine \(M\) with input stack \(k_0\) and output stack \(k_1\), let \(x\) and \(Y\) be lists of symbols of \(k_0\), let \(m, T \in \mathbb{N}\) with \(|x| \le m\), and let \(\alpha\) be a symbol of \(k_1\) that is one of the effective symbols of \(E\) for \(k_1\). Put \(H = m + (T + 1)d + 1\), where \(d\) is the window depth of \(M\), and let \(N\) be the number of situations of \(E\). Suppose an assignment \(a\) satisfies, at bounds \(T\) and \(H\), the update family (the transition clause family of the layout of \(E\) with tables \(\mathrm{la}, \mathrm{na}, \mathrm{wa}\) and \(N\) situations), the S-definition family (the same with \(\mathrm{sa}\) in place of \(\mathrm{na}\)), 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 \(\alpha\). Then there is a list \(y\) whose entries all occur in \(Y\) such that \(|xy| \le m\) and the idle-extended run of \(M\) from the initial configuration on input \(xy\) is, after \(T\) steps, an accepting configuration for \(\alpha\).

Apart from the accept family, no one-hot or at-most-one clauses are assumed.

theorem accept_sound {x Ys : List (M.Γ M.k₀)} {m T : ℕ} {acc : M.Γ M.k₁} {a : List Bool}
    (hx : x.length ≤ m) (hacc : ∃ i, E.dec M.k₁ i = acc)
    (hu : cnfSat (Family.family E.layout E.la E.na E.wa T (capH m T (depth M)) E.N) a)
    (hs : cnfSat (Family.family E.layout E.la E.sa E.wa T (capH m T (depth M)) E.N) a)
    (ha : cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T (capH m T (depth M))) a)
    (hI : cnfSat (E.initFamily x Ys m T (capH m T (depth M))) a)
    (hA : cnfSat (E.accFamily acc T (capH m T (depth M))) a) :
    ∃ y : List (M.Γ M.k₀), (∀ z ∈ y, z ∈ Ys) ∧ (x ++ y).length ≤ m ∧
      Accepts M (runI M (initList M (x ++ y)) T) acc

Uses 31 · Used by 2

Statement usesThe 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 · 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 usesCell literals of an array hold in a row · The code of a configuration holds in a row · Good configurations · Accept-cell clauses pin the top output symbol · Accept-code clauses pin the (label, state) code · 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 · A satisfying assignment tracks a certified run

Used byNo accepting certificate, no satisfying assignment · The five Cook–Levin clause families are satisfiable iff some certificate is accepted

TheoremNo accepting certificate, no satisfying assignment#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with window depth \(d\), let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), let \(m, T \in \mathbb{N}\) with \(|x| \le m\), let \(H = m + (T + 1)d + 1\), and let \(\alpha\) be a symbol of the output stack of \(M\) in the effective alphabet of \(E\). Write \(\mathrm{la}, \mathrm{na}, \mathrm{sa}, \mathrm{wa}, \mathrm{pl}, \mathrm{cn}, \mathrm{pu}\) for the situation tables of \(E\) and \(N\) for its number of situations. Suppose that for no list \(y\) of symbols, each in \(Y\), with \(|xy| \le m\), the configuration after \(T\) steps of the idle-extended run of \(M\) from the initial configuration on input \(xy\) is an accepting configuration for \(\alpha\). Then no assignment satisfies all five of the following families at bounds \(T\) and \(H\): the transition clause family of the layout of \(E\) for \(N\) situations with tables \(\mathrm{la}\), \(\mathrm{na}\), \(\mathrm{wa}\) (the update family); the transition clause family for \(N\) situations with tables \(\mathrm{la}\), \(\mathrm{sa}\), \(\mathrm{wa}\) (the S-definition family); the cell-shift clause family for \(N\) situations with tables \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\); the init family of \(E\) for \(x\), \(Y\), \(m\); and the accept family of \(E\) for \(\alpha\).

In particular, the all-true assignment does not satisfy all five.

theorem unsat_of_noAccept {x Ys : List (M.Γ M.k₀)} {m T : ℕ} {acc : M.Γ M.k₁}
    (hx : x.length ≤ m) (hacc : ∃ i, E.dec M.k₁ i = acc)
    (hno : ¬ ∃ y : List (M.Γ M.k₀), (∀ z ∈ y, z ∈ Ys) ∧ (x ++ y).length ≤ m ∧
      Accepts M (runI M (initList M (x ++ y)) T) acc) (a : List Bool) :
    ¬ (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 20

Statement usesThe 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 · 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 usesSatisfying assignments yield accepting runs

TheoremThe all-true assignment satisfies the transition, shift and init families#✓fully proved

Let \(E\) be an encoding of a machine \(M\) with window depth \(d\), let \(x\) and \(Y\) be lists of symbols of the input stack of \(M\), and let \(m, T, H \in \mathbb{N}\) with \(|x| \le m < H\) and \(d \le H\). Write \(\mathrm{la}, \mathrm{na}, \mathrm{sa}, \mathrm{wa}, \mathrm{pl}, \mathrm{cn}, \mathrm{pu}\) for the situation tables of \(E\), \(N\) for its number of situations and \(V\) for the number of variables of its layout at bounds \(T\) and \(H\). Then the all-true assignment of length \(V\) satisfies each of the following families at bounds \(T\) and \(H\): the transition clause family of the layout of \(E\) for \(N\) situations with tables \(\mathrm{la}\), \(\mathrm{na}\), \(\mathrm{wa}\) (the update family); the transition clause family for \(N\) situations with tables \(\mathrm{la}\), \(\mathrm{sa}\), \(\mathrm{wa}\) (the S-definition family); the cell-shift clause family for \(N\) situations with tables \(\mathrm{sa}\), \(\mathrm{pl}\), \(\mathrm{cn}\), \(\mathrm{pu}\); and the init family of \(E\) for \(x\), \(Y\), \(m\).

Every clause of these families has a positive literal at an index below \(V\).

theorem trans_allTrue {x Ys : List (M.Γ M.k₀)} {m T H : ℕ} (hx : x.length ≤ m) (hmH : m < H)
    (hH : depth M ≤ H) :
    cnfSat (Family.family E.layout E.la E.na E.wa T H E.N) (List.replicate (E.layout.numVars T H) true) ∧
    cnfSat (Family.family E.layout E.la E.sa E.wa T H E.N) (List.replicate (E.layout.numVars T H) true) ∧
    cnfSat (Shift.shFamily E.layout E.sa E.pl E.cn E.pu E.N T H) (List.replicate (E.layout.numVars T H) true) ∧
    cnfSat (E.initFamily x Ys m T H) (List.replicate (E.layout.numVars T H) true)

Uses 52

Statement usesNumber of variables of the transition-clause formula · The transition clause family · The cell-shift clause family · Encoding data for a finite TM2 machine · Number of situations · 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 · Position of a situation's variable · Window symbol code of a situation · Window depth of a machine · 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 · Variables per time step · Index of a label/state variable · Well-formed situation tables for the transition clauses · 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 · 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 · The init family is faithful with positive literals · The situation-definition tables of a machine are well formed · The cell-shift tables of a machine are well formed · The transition tables of a machine are well formed · Faithful literal list · Faithful dense clause family with positive literals · The all-true assignment satisfies a faithful clause with a positive literal · Dense CNF formula · Dense clause · Satisfaction of a dense clause

TheoremThe all-true assignment violates the accept family#✓fully proved

Let \(E\) be an encoding of a finite stack machine \(M\), let \(\alpha\) be a symbol of the output stack of \(M\), and let \(T, H \in \mathbb{N}\). The assignment that sets all \(V\) variables to true, where \(V\) is the number of variables of the layout of \(E\) at bounds \(T\) and \(H\), does not satisfy the accept family for \(\alpha\) at bounds \(T\) and \(H\).

theorem accFamily_allTrue (acc : M.Γ M.k₁) (T H : ℕ) :
    ¬ cnfSat (E.accFamily acc T H) (List.replicate (E.layout.numVars T H) true)

Uses 13

Statement usesNumber of variables of the transition-clause formula · Encoding data for a finite TM2 machine · The accept family · Clause layout of a machine encoding · Satisfaction of a dense CNF formula

Proof usesVariable layout of the transition clauses · Variables per time step · Index of a label/state variable · Number of situations · Accept-code clauses pin the (label, state) code · Accepting code · Truth of a variable under an assignment · Variables of rows up to the time bound

TheoremUnfolding the idle-extended run from the front#✓fully proved

For a finite TM2 machine \(M\), a configuration \(c\) and every \(n \in \mathbb{N}\), the configuration at time \(n + 1\) of the idle-extended run of \(M\) from \(c\) equals the configuration at time \(n\) of the idle-extended run of \(M\) from the idle-extended step of \(M\) at \(c\).

theorem runI_succ' (M : FinTM2) (c : M.Cfg) : ∀ n, runI M c (n + 1) = runI M (stepI M c) n

Uses 2 · Used by 1

Statement usesIdle-extended run · Idle-extended step

Used byThe idle-extended run follows the real run

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.