HAMPATH emitter, phase A: one literal to Moving the tokens back in the HAMPATH emitter

TheoremHAMPATH emitter, phase A: one literal#✓fully proved

For \(x \in \mathbb{N}\) write \(\mathrm{name}(x)\) for the canonical binary encoding of \(x\) as name-bit symbols. Let \(\ell = (x, p)\) be a literal with variable \(x\) and polarity \(p\): its tokens are \(\mathrm{name}(x)\) followed by the polarity marker \(\mathrm{lit}(p)\), and its reversed tokens \(r_\ell\) are \(\mathrm{lit}(p)\) followed by the reverse of \(\mathrm{name}(x)\). For a list \(\mathit{vs}\) of naturals write \(\mathrm{vstk}(\mathit{vs})\) for the names of the entries of \(\mathit{vs}\), each followed by the separator \(\mathrm{cl}\), and \(\mathrm{ins}(x, \mathit{vs})\) for \(\mathit{vs}\) if \(x\) occurs in \(\mathit{vs}\) and for \(\mathit{vs}\) with \(x\) added at the front otherwise. Let \(R\) be a list of symbols that is empty or does not start with a name bit, let \(\mathit{vs}\) be a list of naturals, and let \(s\) be a quiescent state of the HAMPATH emitter whose stack \(T\) is \(r_\ell\) followed by \(R\), whose stack \(V\) is \(\mathrm{vstk}(\mathit{vs})\) and whose stacks \(W\) and \(X\) are empty. Then for every value \(v\) of the machine's Boolean variable there is a value \(v'\) such that the emitter goes in at most \(8|\mathrm{vstk}(\mathit{vs})| + 4|r_\ell| + 8\) steps from label \(\mathrm{a0}\), variable \(v\) and the stacks of \(s\) to label \(\mathrm{a0}\), variable \(v'\) and the stacks of the state obtained from \(s\) by setting \(T\) to \(R\), \(F\) to the tokens of \(\ell\) followed by the old contents of \(F\), and \(V\) to \(\mathrm{vstk}(\mathrm{ins}(x, \mathit{vs}))\).

theorem alit_run (l : ℕ × Bool) (R : List Sym) (hR : R.head?.bind Sym.bit? = none)
    (vs : List ℕ) (s : MS) (v : Bool) (ht : s.t = Check.litRev l ++ R) (hv : s.v = vstk vs)
    (hw : s.w = []) (hx : s.x = []) :
    ∃ v', RunLe prog (8 * (vstk vs).length + 4 * (Check.litRev l).length + 8)
      ⟨some .a0, v, s.stk⟩
      ⟨some .a0, v', {s with t := R, f := litToks l ++ s.f, v := vstk (insV l.1 vs)}.stk⟩

Uses 24 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Insert a variable if new · The HAMPATH emitter machine · Variable stack of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · A literal's tokens on the token stack · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Tokens of a literal · Runs within a step budget

Proof usesHAMPATH emitter, phase A: moving the walk stack back onto the variable stack · HAMPATH emitter, phase A: copying a reversed name onto two stacks · HAMPATH emitter, phase A: searching the variable stack for a name · Variable-stack symbols of the HAMPATH emitter · Name of a variable in the HAMPATH emitter · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Running the bit-moving loop · Pushing a list of symbols onto one stack

Used byHAMPATH emitter, phase A: the literals of a clause

TheoremHAMPATH emitter, phase A: the literals of a clause#✓fully proved

Notation: \(\mathrm{name}(x)\) is the canonical binary encoding of \(x \in \mathbb{N}\) as name-bit symbols; a literal \(\ell = (x, p)\) has tokens \(\mathrm{name}(x)\) followed by the polarity marker \(\mathrm{lit}(p)\) and reversed tokens \(r_\ell\), namely \(\mathrm{lit}(p)\) followed by the reverse of \(\mathrm{name}(x)\); \(\mathrm{vstk}(\mathit{vs})\) is the list of the names of the entries of a list \(\mathit{vs}\) of naturals, each followed by the separator \(\mathrm{cl}\); and \(\mathrm{ins}(x, \mathit{vs})\) is \(\mathit{vs}\) if \(x\) occurs in \(\mathit{vs}\) and \(\mathit{vs}\) with \(x\) added at the front otherwise. Let \(L_b \in \mathbb{N}\), let \(\ell_1, \dots, \ell_k\) be literals with variables \(x_1, \dots, x_k\), let \(n = |r_{\ell_1}| + \dots + |r_{\ell_k}|\), and let \(R\) be a list of symbols that is empty or does not start with a name bit. Then for every list \(\mathit{vs}\) of naturals with \(|\mathrm{vstk}(\mathit{vs})| + n \le L_b\), every quiescent state \(s\) of the HAMPATH emitter whose stack \(T\) is the concatenation of \(r_{\ell_k}, \dots, r_{\ell_1}\) followed by \(R\), whose stack \(V\) is \(\mathrm{vstk}(\mathit{vs})\) and whose stacks \(W\) and \(X\) are empty, and every value \(v\) of the machine's Boolean variable, there is a value \(v'\) such that the emitter goes in at most \(n(8L_b + 12)\) steps from label \(\mathrm{a0}\), variable \(v\) and the stacks of \(s\) to label \(\mathrm{a0}\), variable \(v'\) and the stacks of the state obtained from \(s\) by setting \(T\) to \(R\), \(F\) to the concatenated tokens of \(\ell_1, \dots, \ell_k\) followed by the old contents of \(F\), and \(V\) to \(\mathrm{vstk}(\mathrm{ins}(x_1, \dots \mathrm{ins}(x_k, \mathit{vs}) \dots))\).

theorem alits_run (Lb : ℕ) : ∀ (Ls : List (ℕ × Bool)) (R : List Sym),
    R.head?.bind Sym.bit? = none → ∀ (vs : List ℕ) (s : MS) (v : Bool),
    s.t = Ls.reverse.flatMap Check.litRev ++ R → s.v = vstk vs → s.w = [] → s.x = [] →
    (vstk vs).length + (Ls.flatMap Check.litRev).length ≤ Lb →
    ∃ v', RunLe prog ((Ls.flatMap Check.litRev).length * (8 * Lb + 12)) ⟨some .a0, v, s.stk⟩
      ⟨some .a0, v', { s with
        t := R, f := Ls.flatMap litToks ++ s.f,
        v := vstk (Ls.foldr (fun (l : ℕ × Bool) vs => insV l.1 vs) vs) }.stk⟩

Uses 16 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Insert a variable if new · The HAMPATH emitter machine · Variable stack of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · A literal's tokens on the token stack · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Tokens of a literal · Runs within a step budget

Proof usesHAMPATH emitter, phase A: one literal · Name of a variable in the HAMPATH emitter · Exact-length runs of a TM2 machine

Used byHAMPATH emitter, phase A: one clause

TheoremHAMPATH emitter, phase A: one clause#✓fully proved

Notation: \(\mathrm{name}(x)\) is the canonical binary encoding of \(x \in \mathbb{N}\) as name-bit symbols; a literal \(\ell = (x, p)\) has tokens \(\mathrm{name}(x)\) followed by the polarity marker \(\mathrm{lit}(p)\) and reversed tokens \(r_\ell\), namely \(\mathrm{lit}(p)\) followed by the reverse of \(\mathrm{name}(x)\); \(\mathrm{vstk}(\mathit{vs})\) is the list of the names of the entries of a list \(\mathit{vs}\) of naturals, each followed by the separator \(\mathrm{cl}\); and \(\mathrm{ins}(x, \mathit{vs})\) is \(\mathit{vs}\) if \(x\) occurs in \(\mathit{vs}\) and \(\mathit{vs}\) with \(x\) added at the front otherwise. Let \(L_b \in \mathbb{N}\) and let \(C\) be a clause with literals \(\ell_1, \dots, \ell_k\) and variables \(x_1, \dots, x_k\). The tokens of \(C\) are the concatenated tokens of \(\ell_1, \dots, \ell_k\) followed by \(\mathrm{cl}\), and its reversed tokens \(r_C\) are \(\mathrm{cl}\) followed by the concatenation of \(r_{\ell_k}, \dots, r_{\ell_1}\). Let \(R\) be a list of symbols that is empty or starts with \(\mathrm{cl}\), let \(\mathit{vs}\) be a list of naturals with \(|\mathrm{vstk}(\mathit{vs})| + |r_C| \le L_b\), and let \(s\) be a quiescent state of the HAMPATH emitter whose stack \(T\) is \(r_C\) followed by \(R\), whose stack \(V\) is \(\mathrm{vstk}(\mathit{vs})\) and whose stacks \(W\) and \(X\) are empty. Then for every value \(v\) of the machine's Boolean variable there is a value \(v'\) such that the emitter goes in at most \(|r_C|(8L_b + 12)\) steps from label \(\mathrm{a0}\), variable \(v\) and the stacks of \(s\) to label \(\mathrm{a0}\), variable \(v'\) and the stacks of the state obtained from \(s\) by setting \(T\) to \(R\), \(F\) to the tokens of \(C\) followed by the old contents of \(F\), and \(V\) to \(\mathrm{vstk}(\mathrm{ins}(x_1, \dots \mathrm{ins}(x_k, \mathit{vs}) \dots))\), and by increasing the clause count by \(1\) and the triple clause count by \(3\).

theorem aclause_run (Lb : ℕ) (C : CNFClause) (R : List Sym) (hR : R = [] ∨ R.head? = some .cl)
    (vs : List ℕ) (s : MS) (v : Bool) (ht : s.t = Check.clRev C ++ R) (hv : s.v = vstk vs)
    (hw : s.w = []) (hx : s.x = []) (hb : (vstk vs).length + (Check.clRev C).length ≤ Lb) :
    ∃ v', RunLe prog ((Check.clRev C).length * (8 * Lb + 12)) ⟨some .a0, v, s.stk⟩
      ⟨some .a0, v', { s with
        t := R, f := clauseToks C ++ s.f, v := vstk ((C.map Prod.fst).foldr insV vs),
        c := s.c + 1, mm := s.mm + 3 }.stk⟩

Uses 20 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Insert a variable if new · The HAMPATH emitter machine · Variable stack of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · A clause's tokens on the token stack · Stack alphabet of the SAT verifier · Tokens of a clause · CNF clause · Runs within a step budget

Proof usesHAMPATH emitter, phase A: the literals of a clause · A literal's tokens on the token stack · Reading a symbol as a name bit · Tokens of a literal · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Pushing a list of symbols onto one stack

Used byHAMPATH emitter, phase A: the clauses of a formula

TheoremHAMPATH emitter, phase A: the clauses of a formula#✓fully proved

Notation: \(\mathrm{name}(x)\) is the canonical binary encoding of \(x \in \mathbb{N}\) as name-bit symbols; a literal \(\ell = (x, p)\) has tokens \(\mathrm{name}(x)\) followed by the polarity marker \(\mathrm{lit}(p)\); a clause \(C\) with literals \(\ell_1, \dots, \ell_k\) has tokens the concatenated tokens of \(\ell_1, \dots, \ell_k\) followed by the separator \(\mathrm{cl}\), and reversed tokens \(r_C\), namely \(\mathrm{cl}\) followed by, for \(\ell = \ell_k, \dots, \ell_1\) in turn, \(\mathrm{lit}(p)\) and the reverse of \(\mathrm{name}(x)\); \(\mathrm{vstk}(\mathit{vs})\) is the list of the names of the entries of a list \(\mathit{vs}\) of naturals, each followed by \(\mathrm{cl}\); and \(\mathrm{ins}(x, \mathit{vs})\) is \(\mathit{vs}\) if \(x\) occurs in \(\mathit{vs}\) and \(\mathit{vs}\) with \(x\) added at the front otherwise. Let \(L_b \in \mathbb{N}\), let \(\varphi\) be a CNF formula with clauses \(C_1, \dots, C_m\), whose tokens are the concatenated tokens of \(C_1, \dots, C_m\), let \(y_1, \dots, y_n\) be the variables of the literals of \(\varphi\) in order of occurrence (with repetitions), let \(N = |r_{C_1}| + \dots + |r_{C_m}|\), and let \(R\) be a list of symbols that is empty or starts with \(\mathrm{cl}\). Then for every list \(\mathit{vs}\) of naturals with \(|\mathrm{vstk}(\mathit{vs})| + N \le L_b\), every quiescent state \(s\) of the HAMPATH emitter whose stack \(T\) is the concatenation of \(r_{C_m}, \dots, r_{C_1}\) followed by \(R\), whose stack \(V\) is \(\mathrm{vstk}(\mathit{vs})\) and whose stacks \(W\) and \(X\) are empty, and every value \(v\) of the machine's Boolean variable, there is a value \(v'\) such that the emitter goes in at most \(N(8L_b + 12)\) steps from label \(\mathrm{a0}\), variable \(v\) and the stacks of \(s\) to label \(\mathrm{a0}\), variable \(v'\) and the stacks of the state obtained from \(s\) by setting \(T\) to \(R\), \(F\) to the tokens of \(\varphi\) followed by the old contents of \(F\), and \(V\) to \(\mathrm{vstk}(\mathrm{ins}(y_1, \dots \mathrm{ins}(y_n, \mathit{vs}) \dots))\), and by increasing the clause count by \(m\) and the triple clause count by \(3m\).

theorem aformula_run (Lb : ℕ) : ∀ (φ : CNF) (R : List Sym), (R = [] ∨ R.head? = some .cl) →
    ∀ (vs : List ℕ) (s : MS) (v : Bool), s.t = φ.reverse.flatMap Check.clRev ++ R →
    s.v = vstk vs → s.w = [] → s.x = [] →
    (vstk vs).length + (φ.reverse.flatMap Check.clRev).length ≤ Lb →
    ∃ v', RunLe prog ((φ.reverse.flatMap Check.clRev).length * (8 * Lb + 12))
      ⟨some .a0, v, s.stk⟩
      ⟨some .a0, v', { s with
        t := R, f := toks φ ++ s.f, v := vstk ((varsOf φ).foldr insV vs),
        c := s.c + φ.length, mm := s.mm + 3 * φ.length }.stk⟩

Uses 20 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Insert a variable if new · The HAMPATH emitter machine · Variable stack of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · A clause's tokens on the token stack · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · Occurrence list of a CNF formula · CNF formula · CNF clause · Runs within a step budget

Proof usesHAMPATH emitter, phase A: one clause · Name of a variable in the HAMPATH emitter · A literal's tokens on the token stack · Tokens of a clause · Exact-length runs of a TM2 machine

Used byPhase A of the HAMPATH emitter

DefinitionInitial state of the HAMPATH emitter#✓fully proved

For a CNF formula \(\varphi\) and an output list \(o\), the initial state is the quiescent state whose token stack holds the tokens of \(\varphi\) in reverse reading order, whose output stack is \(o\), and all of whose other stacks are empty and counters zero.

def initMS (φ : CNF) (o : List Bool) : MS :=
  ⟨(toks φ).reverse, o, [], [], [], [], [], [], 0, 0, 0, 0, 0, 0, 0, 0⟩

Uses 4 · Used by 2

Statement usesQuiescent states of the HAMPATH emitter · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula

Used byPhase A of the HAMPATH emitter · Correctness and running time of the HAMPATH emitter

DefinitionThe emitter state before the diamonds#✓fully proved

For a CNF formula \(\varphi\) with \(m\) clauses and an output list \(o\), this is the quiescent state whose output stack is \(o\), whose stack \(F\) holds the tokens of \(\varphi\) in reading order, whose stack \(V\) is the variable stack of the distinct variables of \(\varphi\) (each kept at its last occurrence), whose clause count and diamond top are both \(m\), whose count of three times the clauses is \(3m\), and all of whose other stacks are empty and other counters zero.

It is the state that phase A, followed by setting the diamond top, reaches from the initial state.

def diaMS (φ : CNF) (o : List Bool) : MS :=
  ⟨[], o, toks φ, vstk (hamVars φ), [], [], [], [], φ.length, 3 * φ.length, φ.length, 0, 0, 0,
    0, 0⟩

Uses 7 · Used by 2

Statement usesQuiescent states of the HAMPATH emitter · Variable stack of the HAMPATH emitter · Distinct variables of a formula · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · CNF clause

Used byPhase A of the HAMPATH emitter · Correctness and running time of the HAMPATH emitter

TheoremPhase A of the HAMPATH emitter#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses whose token list has length \(L\), let \(o\) be a list of bits and let \(v\) be a bit. Started at label \(\mathrm{a0}\) with internal state \(v\) and the stacks of the initial emitter state of \(\varphi\) and \(o\) (the token stack holding the tokens of \(\varphi\) reversed, the output stack holding \(o\), and everything else empty), the emitter reaches, within at most \(L(8L + 12) + 2m + 3\) steps, label \(\mathrm{h0}\) with some internal state and the stacks of the emitter state of \(\varphi\) and \(o\) after phase A (the tokens of \(\varphi\) on \(F\), the variable stack of the distinct variables of \(\varphi\) on \(V\), \(m\) on the counters \(C\) and \(P\), \(3m\) on \(M\), \(o\) on the output stack, and everything else empty).

theorem phaseA_run (φ : CNF) (o : List Bool) (v : Bool) :
    ∃ v', RunLe prog ((toks φ).length * (8 * (toks φ).length + 12) + 2 * φ.length + 3)
      ⟨some .a0, v, (initMS φ o).stk⟩ ⟨some .h0, v', (diaMS φ o).stk⟩

Uses 29 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Stacks of a quiescent emitter state · The emitter state before the diamonds · Initial state of the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · CNF clause · Runs within a step budget

Proof usesQuiescent states of the HAMPATH emitter · HAMPATH emitter, phase A: the clauses of a formula · Copying a counter in the HAMPATH emitter · Removing duplicates by insertion · Insert a variable if new · Name of a variable in the HAMPATH emitter · Variable stack of the HAMPATH emitter · Distinct variables of a formula · A clause's tokens on the token stack · A literal's tokens on the token stack · Tokens of a clause · Tokens of a literal · Occurrence list of a CNF formula · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Unary counter · Pushing a list of symbols onto one stack

Used byCorrectness and running time of the HAMPATH emitter

DefinitionToken symbols of the HAMPATH emitter#✓fully proved

A symbol is a token when it is a name bit, a polarity marker or the clause separator \(\mathsf{cl}\); the value markers and the dead marker are not tokens. The emitter moves tokens between its stacks \(T\) and \(F\).

def isTok : Sym → Bool
  | .bit _ | .lit _ | .cl => true
  | _ => false

Uses 1 · Used by 2

Statement usesStack alphabet of the SAT verifier

Used byMoving the tokens back in the HAMPATH emitter · End of a diamond

TheoremThe tokens of a literal do not start with a clause end#✓fully proved

For every literal \((n, p)\) with variable index \(n \in \mathbb{N}\) and polarity \(p\), the token list of \((n, p)\) is nonempty and its first symbol is not the clause-end marker \(\mathsf{cl}\).

theorem litToks_head (l : ℕ × Bool) : ∃ x R, litToks l = x :: R ∧ x ≠ .cl

Uses 2 · Used by 1

Statement usesStack alphabet of the SAT verifier · Tokens of a literal

Used byOne literal of the detour walk

TheoremOne literal of the detour walk#✓fully proved

Let \(y \in \mathbb{N}\) have binary encoding \(\mathrm{bin}(y)\), let \(l = (z, b)\) be a literal with token list \(\tau\), let \(\rho\) and \(\nu\) be lists of symbols, let \(p_+\), \(p_-\) and \(v\) be bits, and let \(s\) be a quiescent state of the HAMPATH emitter such that \(F\) holds \(\tau\) followed by \(\rho\), \(V\) holds the name of \(y\), then the clause symbol \(\mathrm{cl}\), then \(\nu\), and the scratch stack \(X\) is empty. Then there is a bit \(v'\) such that the emitter goes in at most \(3|\mathrm{bin}(y)| + |\tau| + 5\) steps from the detour-walk label with clause flags \((p_+, p_-)\), state bit \(v\) and the stacks of \(s\) to the detour-walk label with clause flags \((p_+ \lor (z = y \land b), p_- \lor (z = y \land \lnot b))\) and state bit \(v'\), with the stacks of \(s\) changed as follows: \(F\) becomes \(\rho\) and \(\tau\) reversed is prepended to \(T\).

theorem dlit_run (y : ℕ) (VR : List Sym) (l : ℕ × Bool) (R : List Sym) (pp pn : Bool) (s : MS)
    (v : Bool) (hf : s.f = litToks l ++ R) (hv : s.v = name y ++ Sym.cl :: VR) (hx : s.x = []) :
    ∃ v', RunLe prog (3 * (encodeNat y).length + (litToks l).length + 5)
      ⟨some (.dw pp pn), v, s.stk⟩
      ⟨some (.dw (pp || (decide (l.1 = y) && l.2)) (pn || (decide (l.1 = y) && !l.2))), v',
        {s with f := R, t := (litToks l).reverse ++ s.t}.stk⟩

Uses 20 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Name of a variable in the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Tokens of a literal · Runs within a step budget

Proof usesEnd of a clause in the detour walk · Comparing a name with the top entry of the variable stack · The tokens of a literal do not start with a clause end · Reading a symbol as a name bit · The binary code of natural numbers is injective · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Running the bit-moving loop

Used byThe literals of a clause in the detour walk

TheoremThe literals of a clause in the detour walk#✓fully proved

Let \(y \in \mathbb{N}\) have binary encoding \(\mathrm{bin}(y)\) and let \(\nu\) and \(\rho\) be lists of symbols. For every list \(C\) of literals with token list \(\tau\) (the tokens of its literals in order, without a clause separator), all bits \(p_+, p_-, b\), and every quiescent state \(s\) of the emitter such that \(F\) holds \(\tau\) followed by \(\rho\), \(V\) holds the name of \(y\), then a clause separator, then \(\nu\), and the scratch stack \(X\) is empty, there is a state bit \(b'\) such that the emitter goes in at most \(|\tau|(3|\mathrm{bin}(y)| + 6)\) steps from the detour-walk label with clause flags \((p_+, p_-)\), state bit \(b\) and the stacks of \(s\) to the detour-walk label with clause flags \((p_+ \lor ((y, \mathrm{true}) \in C), p_- \lor ((y, \mathrm{false}) \in C))\) and state bit \(b'\), with the stacks of \(s\) changed as follows: \(F\) becomes \(\rho\) and \(\tau\) reversed is prepended to \(T\).

theorem dlits_run (y : ℕ) (VR : List Sym) (R : List Sym) :
    ∀ (Ls : List (ℕ × Bool)) (pp pn : Bool) (s : MS) (v : Bool),
      s.f = Ls.flatMap litToks ++ R → s.v = name y ++ Sym.cl :: VR → s.x = [] →
      ∃ v', RunLe prog ((Ls.flatMap litToks).length * (3 * (encodeNat y).length + 6))
        ⟨some (.dw pp pn), v, s.stk⟩
        ⟨some (.dw (pp || decide ((y, true) ∈ Ls)) (pn || decide ((y, false) ∈ Ls))), v',
          {s with f := R, t := (Ls.flatMap litToks).reverse ++ s.t}.stk⟩

Uses 12 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Name of a variable in the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Tokens of a literal · Runs within a step budget

Proof usesOne literal of the detour walk · Exact-length runs of a TM2 machine

Used byOne clause of the detour walk

TheoremOne clause of the detour walk#✓fully proved

Let \(B, m, i, y, j \in \mathbb{N}\), let \(C\) be a clause with token list \(\mathrm{toks}(C)\), let \(\rho\) and \(\nu\) be lists of symbols and \(b\) a state bit, and let \(s\) be a quiescent state of the emitter such that \(F\) holds \(\mathrm{toks}(C)\) followed by \(\rho\), \(V\) holds the name of \(y\), then a clause separator, then \(\nu\), the scratch stack \(X\) is empty, the counter \(J\) equals \(j\), the counter \(D\) equals row vertex \(3j + 1\) of diamond \(i\) for \(m\) clauses, each of the counters \(P, N, R, J, D\) is at most \(B\), and the binary encoding of \(y\) has length at most \(B\). Then for some state bit \(b'\) the emitter goes in at most \(|\mathrm{toks}(C)|(3B + 6) + 16B + 26\) steps from the detour-walk label with both clause flags false, state bit \(b\) and the stacks of \(s\) back to the same label with state bit \(b'\) and the stacks of \(s\) changed as follows: \(F\) becomes \(\rho\), \(\mathrm{toks}(C)\) reversed is prepended to \(T\), \(J\) becomes \(j + 1\), \(D\) increases by \(3\), and the edge-bit list \(q\) is extended by the bits of the detour arcs of clause \(j\) (contents \(C\)) in diamond \(i\) for variable \(y\).

theorem dclause_run (Bd m dI y j : ℕ) (C : CNFClause) (R VR : List Sym) (s : MS) (v : Bool)
    (hf : s.f = clauseToks C ++ R) (hv : s.v = name y ++ Sym.cl :: VR) (hx : s.x = [])
    (hj : s.j = j) (hd : s.d = hpR m dI (3 * j + 1)) (hB : ∀ u, s.val u ≤ Bd)
    (hy : (encodeNat y).length ≤ Bd) :
    ∃ v', RunLe prog ((clauseToks C).length * (3 * Bd + 6) + 16 * Bd + 26)
      ⟨some (.dw false false), v, s.stk⟩
      ⟨some (.dw false false), v', { s with
        f := R, t := (clauseToks C).reverse ++ s.t, j := j + 1, d := s.d + 3,
        q := s.q ++ Karp.edgeBits (detE m dI y j C) }.stk⟩

Uses 31 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Counter values of a quiescent emitter state · Counters read by HAMPATH copy sites · Clause detours in a diamond · Name of a variable in the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Bit encoding of an edge list · Row vertices of a diamond · Stack alphabet of the SAT verifier · Tokens of a clause · CNF clause · Runs within a step budget

Proof usesCopy sites chained in the HAMPATH emitter · Copy sites of the HAMPATH emitter · Extra ones of a copy site · Counter read by a copy site · Bits pushed by a copy site of the HAMPATH emitter · Step count of a list of copy sites in the HAMPATH emitter · Running a chain of copy sites in the HAMPATH emitter · End of a clause in the detour walk · The literals of a clause in the detour walk · Consecutive row vertices · Bits of concatenated edge lists · Tokens of a literal · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Pushing a list of symbols onto one stack

Used byThe detour walk of a diamond in the HAMPATH emitter

TheoremThe detour walk of a diamond in the HAMPATH emitter#✓fully proved

Let \(B\), \(m\), \(i\) and \(y\) be natural numbers and \(\varphi = C_0 \cdots C_{m-1}\) a CNF formula with \(m\) clauses. Write \(\tau = m + i(3m+2)\) for the top vertex of diamond \(i\) and \(\rho_l = \tau + 1 + l\) for its row vertices, encode an arc \((a, b)\) by the bits \(1^a 0 1^b 0\), write \(\mathrm{toks}(\psi)\) for the token sequence of a list of clauses \(\psi\), and call the bits of the binary code \(\mathrm{enc}(y)\) of \(y\), as symbols, the name bits of \(y\). The detour arcs of clause \(j\) are \((\rho_{3j+1}, j)\) and \((j, \rho_{3j+2})\) if the literal \((y, \mathrm{true})\) is in \(C_j\), followed by \((\rho_{3j+2}, j)\) and \((j, \rho_{3j+1})\) if \((y, \mathrm{false})\) is in \(C_j\). Let \(\sigma\) be a list of symbols and \(q_0\) a list of bits, and suppose \(|\mathrm{enc}(y)| \le B\) and \(\rho_{3m} \le B\). Then for every splitting \(\varphi = \pi \kappa\) into a prefix \(\pi\) and a suffix \(\kappa\) of clauses, every quiescent state \(s\) of the emitter and every internal bit \(v\): if \(F\) holds \(\mathrm{toks}(\kappa)\), \(T\) holds \(\mathrm{toks}(\pi)\) reversed, \(V\) holds the name bits of \(y\) followed by the separator \(\mathsf{cl}\) and then \(\sigma\), \(X\) is empty, \(J = |\pi|\), \(D = \rho_{3|\pi|+1}\), the edge bits are \(q_0\) followed by the codes of the detour arcs of the clauses \(j < |\pi|\) in increasing order of \(j\), and \(P\), \(N\), \(R\) are at most \(B\), then there is an internal bit \(v'\) such that the emitter goes, in at most \(|\mathrm{toks}(\kappa)|(3B+6) + |\kappa|(16B+26) + 1\) steps, from label \(\mathsf{dw}(\mathrm{false}, \mathrm{false})\) with bit \(v\) and the stacks of \(s\) to label \(\mathsf{t0}\) with bit \(v'\) and the stacks of the state obtained from \(s\) by emptying \(F\), setting \(T\) to \(\mathrm{toks}(\varphi)\) reversed, \(J = m\) and \(D = \rho_{3m+1}\), and setting the edge bits to \(q_0\) followed by the codes of the detour arcs of the clauses \(j < m\) in increasing order of \(j\).

theorem dwalk_run (Bd m dI y : ℕ) (φ : CNF) (hm : φ.length = m) (VR : List Sym)
    (q0 : List Bool) (hy : (encodeNat y).length ≤ Bd) (hR : hpR m dI (3 * m) ≤ Bd) :
    ∀ (post pre : CNF), φ = pre ++ post → ∀ (s : MS) (v : Bool), s.f = toks post →
      s.t = (toks pre).reverse → s.v = name y ++ Sym.cl :: VR → s.x = [] →
      s.j = pre.length → s.d = hpR m dI (3 * pre.length + 1) →
      s.q = q0 ++ Karp.edgeBits ((List.range pre.length).flatMap
        (fun j => detE m dI y j (φ.getD j []))) →
      s.p ≤ Bd → s.n ≤ Bd → s.r ≤ Bd →
      ∃ v', RunLe prog ((toks post).length * (3 * Bd + 6) + post.length * (16 * Bd + 26) + 1)
        ⟨some (.dw false false), v, s.stk⟩
        ⟨some .t0, v', { s with
          f := [], t := (toks φ).reverse, j := m, d := hpR m dI (3 * m + 1),
          q := q0 ++ Karp.edgeBits ((List.range m).flatMap
            (fun j => detE m dI y j (φ.getD j []))) }.stk⟩

Uses 25 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Clause detours in a diamond · Name of a variable in the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Bit encoding of an edge list · Row vertices of a diamond · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · CNF clause · Runs within a step budget

Proof usesCounter values of a quiescent emitter state · Counters read by HAMPATH copy sites · End of a clause in the detour walk · One clause of the detour walk · Splitting off the middle clause of a concatenation · Bits of concatenated edge lists · Tops of the diamonds · Tokens of a clause · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byThe detours of a diamond

DefinitionFrame copy sites of the HAMPATH emitter#✓fully proved

The list of the eight copy sites of a diamond's frame arcs, in order: the source site and then the target site of the first, second, third and fourth frame arc.

def frameSites : List Site := [.f1u, .f1v, .f2u, .f2v, .f3u, .f3v, .f4u, .f4v]

Uses 1 · Used by 1

Statement usesCopy sites of the HAMPATH emitter

Used byFront of a diamond

DefinitionRow copy sites of the HAMPATH emitter#✓fully proved

The list of the four copy sites of the two row arcs between consecutive row vertices of a diamond, in order: the source site and then the target site of the first and of the second row arc.

def rowSites : List Site := [.w1u, .w1v, .w2u, .w2v]

Uses 1 · Used by 1

Statement usesCopy sites of the HAMPATH emitter

Used byThe row loop of a diamond in the HAMPATH emitter

TheoremFront of a diamond#✓fully proved

Let \(B, m, i \in \mathbb{N}\), let \(b\) be a state bit, and let \(s\) be a quiescent state of the emitter whose stack \(V\) is nonempty, whose counter \(P\) equals the top of diamond \(i\) for \(m\) clauses, whose counter \(M\) equals \(3m\), whose counter \(N\) is \(0\), and whose counters \(R\), \(J\), \(D\) are at most \(B\), and suppose row vertex \(3m\) of diamond \(i\) is at most \(B\). Then for some state bit \(b'\) the emitter goes in at most \(20B + 30\) steps from label \(\mathrm{h0}\) with state bit \(b\) and the stacks of \(s\) to label \(\mathrm{r0}\) with state bit \(b'\) and the stacks of \(s\) with \(N\) set to row vertex \(3m\) of diamond \(i\) and the edge-bit list \(q\) extended by the bits of the frame arcs of diamond \(i\).

theorem dfront_run (Bd m dI : ℕ) (s : MS) (v : Bool) (x0 : Sym) (R0 : List Sym)
    (hv : s.v = x0 :: R0) (hp : s.p = hpT m dI) (hmm : s.mm = 3 * m) (hn : s.n = 0)
    (hr : s.r ≤ Bd) (hj : s.j ≤ Bd) (hd : s.d ≤ Bd) (hB : hpR m dI (3 * m) ≤ Bd) :
    ∃ v', RunLe prog (20 * Bd + 30) ⟨some .h0, v, s.stk⟩
      ⟨some .r0, v', { s with
        n := hpR m dI (3 * m), q := s.q ++ Karp.edgeBits (frameE m dI) }.stk⟩

Uses 27 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · The frame of a diamond · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Bit encoding of an edge list · Row vertices of a diamond · Tops of the diamonds · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesCopy sites chained in the HAMPATH emitter · Counter values of a quiescent emitter state · Copy sites of the HAMPATH emitter · Extra ones of a copy site · Counter read by a copy site · Counters read by HAMPATH copy sites · Bits pushed by a copy site of the HAMPATH emitter · Step count of a list of copy sites in the HAMPATH emitter · Running a chain of copy sites in the HAMPATH emitter · Copying a counter in the HAMPATH emitter · Frame copy sites of the HAMPATH emitter · The next diamond top follows the row · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Unary counter

Used byOne diamond

TheoremThe row loop of a diamond in the HAMPATH emitter#✓fully proved

Let \(B\), \(m\) and \(i\) be natural numbers, write \(\tau = m + i(3m+2)\) for the top vertex of diamond \(i\) and \(\rho_l = \tau + 1 + l\) for its row vertices, and encode an arc \((a, b)\) by the bits \(1^a 0 1^b 0\). Let \(s\) be a quiescent state of the emitter whose counters satisfy \(M = 3m\), \(L = 0\), \(R = \rho_0\), \(P \le B\), \(N \le B\), \(J \le B\) and \(D \le B\), and suppose \(\rho_{3m} \le B\) and \(3m \le B\). Then for every internal bit \(v\) there is an internal bit \(v'\) such that the emitter goes, in at most \(B(8B+15) + 2\) steps, from label \(\mathsf{r3}\) with bit \(v\) and the stacks of \(s\) to label \(\mathsf{e0}\) with bit \(v'\) and the stacks of the state obtained from \(s\) by setting \(R = \rho_{3m}\) and appending to its edge bits the codes of the arcs \((\rho_l, \rho_{l+1})\) and \((\rho_{l+1}, \rho_l)\) for \(l = 0, \dots, 3m-1\), in this order.

theorem drow_run (Bd m dI : ℕ) (s : MS) (v : Bool) (hmm : s.mm = 3 * m) (hl : s.l = 0)
    (hr : s.r = hpR m dI 0) (hp : s.p ≤ Bd) (hn : s.n ≤ Bd) (hj : s.j ≤ Bd) (hd : s.d ≤ Bd)
    (hB : hpR m dI (3 * m) ≤ Bd) (hmB : 3 * m ≤ Bd) :
    ∃ v', RunLe prog (Bd * (8 * Bd + 15) + 2) ⟨some .r3, v, s.stk⟩
      ⟨some .e0, v', { s with
        r := hpR m dI (3 * m),
        q := s.q ++ Karp.edgeBits ((List.range (3 * m)).flatMap (rowE m dI)) }.stk⟩

Uses 31 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · The HAMPATH emitter machine · The row arcs of a diamond · Stack alphabets of the HAMPATH emitter · Bit encoding of an edge list · Row vertices of a diamond · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesCopy sites chained in the HAMPATH emitter · Counter values of a quiescent emitter state · Copy sites of the HAMPATH emitter · Extra ones of a copy site · Counter read by a copy site · Counters read by HAMPATH copy sites · Bits pushed by a copy site of the HAMPATH emitter · Step count of a list of copy sites in the HAMPATH emitter · Running a chain of copy sites in the HAMPATH emitter · Consecutive row vertices · Row copy sites of the HAMPATH emitter · Bits of concatenated edge lists · Tops of the diamonds · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Unary counter · Exact running time of a for loop over a counter · Sum of consecutive values · Termwise bound on a sum of consecutive values

Used byThe row of a diamond in the HAMPATH emitter

TheoremAdding units along no stacks#✓fully proved

For every \(i \in \mathbb{N}\) and all stack contents \(S\) of the HAMPATH emitter, adding \(i\) units to the stacks named in the empty list of (stack, symbol) pairs leaves \(S\) unchanged: \(\mathrm{addU}([\,], i, S) = S\).

theorem addU_nil (i : ℕ) (S : ∀ k, List (Γ k)) : addU [] i S = S

Uses 3 · Used by 1

Statement usesStacks of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · Adding units to target stacks

Used byDraining a counter

TheoremDraining a counter#✓fully proved

Let \(k\) be a stack of the emitter and \(\ell, \ell'\) labels such that the instruction at \(\ell\) is the transfer loop that pops stack \(k\) until it is empty, pushing nothing, and then goes to \(\ell'\). If \(S\) is an assignment of stack contents in which stack \(k\) consists of \(n\) copies of a symbol \(u\), then for every state bit \(b\) the emitter goes in exactly \(n + 1\) steps from label \(\ell\) with state bit \(b\) and stacks \(S\) to label \(\ell'\) with state bit false and the stacks \(S\) with stack \(k\) emptied.

theorem drain_run {k : K} {self next : Lab} (h : prog self = xfer k [] self next) (u : Γ k)
    (n : ℕ) (v : Bool) (S : ∀ k, List (Γ k)) (hS : S k = cnt u n) :
    Run prog (n + 1) ⟨some self, v, S⟩ ⟨some next, false, update S k []⟩

Uses 11 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Flag bit of a machine state · Exact-length runs of a TM2 machine · Unary counter · Counter transfer loop

Proof usesAdding units along no stacks · Adding units to target stacks · Running a counter transfer

Used byEnd of a diamond

TheoremMoving the tokens back in the HAMPATH emitter#✓fully proved

Let \(L\) be a list of symbols that are all tokens, \(s\) a quiescent state of the emitter whose stack \(T\) holds \(L\), and \(v\) an internal bit. Then there is an internal bit \(v'\) such that the emitter goes in exactly \(|L| + 1\) steps from label \(\mathsf{t0}\) with bit \(v\) and the stacks of \(s\) to label \(\mathsf{t1}\) with bit \(v'\) and the stacks of the state obtained from \(s\) by emptying \(T\) and replacing \(F\) by \(L\) reversed followed by \(F\).

theorem t0_run : ∀ (L : List Sym), (∀ x ∈ L, isTok x = true) → ∀ (s : MS) (v : Bool),
    s.t = L → ∃ v', Run prog (L.length + 1) ⟨some .t0, v, s.stk⟩
      ⟨some .t1, v', {s with t := [], f := L.reverse ++ s.f}.stk⟩

Uses 13 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · Quiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Token symbols of the HAMPATH emitter · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesReading a symbol as a name bit · A single step executes the statement at the current label · Bit on top of a stack · Bit test for the top of a stack

Used byEnd of a diamond

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.