Every vertex of the contracted path except its end has a successor to Second counter of a HAMPATH-verifier comparison

TheoremEvery vertex of the contracted path except its end has a successor#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables. In Sipser's HAMPATH graph for \(\varphi\), clause \(j\) is vertex \(j < m\) and the top of diamond \(i\) is \(t_i = m + i(3m + 2)\). Let \(p\) be a Hamiltonian path of this graph (on the vertices \(0, \dots, t_k\)) from \(t_0\) to \(t_k\), and let \(p'\) be \(p\) with the clause vertices deleted. Then every vertex \(v \ne t_k\) of \(p'\) is immediately followed in \(p'\) by some vertex \(w\).

theorem exists_infix_dropClauses {v : ℕ} (hv : v ∈ dropClauses φ p)
    (hk : v ≠ hpT φ.length (hamVars φ).length) : ∃ w, [v, w] <:+: dropClauses φ p

Uses 8 · Used by 2

Statement usesHamiltonian paths · Deleting the clause vertices from a path · Arcs of the HAMPATH construction · Distinct variables of a formula · Tops of the diamonds · CNF formula · CNF clause

Proof usesArcs of the PATH digraph

Used byEvery top but the last is followed by an end of its row · A row entered at one end is run to the other end

TheoremEntering a row and leaving it at once is impossible#✓fully proved

Let \(\varphi\) be a CNF formula with \(m > 0\) clauses and \(n\) distinct variables. For \(k \le n\) let \(t_k = m + k(3m + 2)\) be the top of diamond \(k\), and for \(k < n\) let row \(k\) consist of the vertices \(t_k + 1 + l\) with \(0 \le l \le 3m\); its left end is \(t_k + 1\) and its right end is \(t_k + 1 + 3m\). Let \(p\) be a Hamiltonian path from \(t_0\) to \(t_n\) in Sipser's digraph for \(\varphi\) on the vertices \(0, \dots, t_n\) whose clause detours are normal: every clause vertex \(j < m\) occurs in \(p\) immediately between the vertices \(t_k + 3j + 2\) and \(t_k + 3j + 3\) of some row \(k < n\), in either order. Let \(q\) be \(p\) with the clause vertices \(0, \dots, m - 1\) deleted. Then for every \(i < n\) and each end \(e\) of row \(i\), it is not the case that in \(q\) the top \(t_i\) is immediately followed by \(e\) and \(e\) is immediately followed by \(t_{i+1}\).

theorem no_shortcut {i : ℕ} {b : Bool} (hi : i < (hamVars φ).length) (hm : 0 < φ.length)
    (hd : DetoursNormal φ p)
    (h1 : [hpT φ.length i, hpRo φ.length i b 0] <:+: dropClauses φ p)
    (h2 : [hpRo φ.length i b 0, hpT φ.length (i + 1)] <:+: dropClauses φ p) : False

Uses 17 · Used by 1

Statement usesNormal clause detours · Hamiltonian paths · Deleting the clause vertices from a path · Arcs of the HAMPATH construction · Distinct variables of a formula · Row vertices counted from either end · Tops of the diamonds · CNF formula · CNF clause

Proof usesIn-neighbours of a row vertex outside the clause vertices · Consecutive vertices of the contracted path are joined by arcs · Row vertices of a diamond · Row vertices lie below the next top · Tops are monotone in the diamond index · Tops of distinct diamonds are at least \(3m + 2\) apart · A Hamiltonian path visits every vertex · Arcs of the PATH digraph

Used byA row entered at one end is run to the other end

TheoremA row entered at one end is run to the other end#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(n\) distinct variables. For \(k \le n\) let \(t_k = m + k(3m + 2)\) be the top of diamond \(k\), and for \(k < n\) let row \(k\) consist of the vertices \(t_k + 1 + l\) with \(0 \le l \le 3m\); its left end is \(t_k + 1\) and its right end is \(t_k + 1 + 3m\). Let \(p\) be a Hamiltonian path from \(t_0\) to \(t_n\) in Sipser's digraph for \(\varphi\) on the vertices \(0, \dots, t_n\) whose clause detours are normal: every clause vertex \(j < m\) occurs in \(p\) immediately between the vertices \(t_k + 3j + 2\) and \(t_k + 3j + 3\) of some row \(k < n\), in either order. Let \(q\) be \(p\) with the clause vertices \(0, \dots, m - 1\) deleted. Let \(i < n\), let \(e\) be an end of row \(i\), and for \(0 \le l \le 3m\) let \(r_l\) be the \(l\)-th vertex of row \(i\) counted from \(e\), that is \(r_l = t_i + 1 + l\) if \(e\) is the left end and \(r_l = t_i + 1 + 3m - l\) if \(e\) is the right end. If the top \(t_i\) is immediately followed by \(r_0\) in \(q\), then for every \(l < 3m\) the vertex \(r_l\) is immediately followed by \(r_{l+1}\) in \(q\).

theorem row_run {i : ℕ} {b : Bool} (hi : i < (hamVars φ).length) (hd : DetoursNormal φ p)
    (h0 : [hpT φ.length i, hpRo φ.length i b 0] <:+: dropClauses φ p) :
    ∀ l < 3 * φ.length,
      [hpRo φ.length i b l, hpRo φ.length i b (l + 1)] <:+: dropClauses φ p

Uses 19 · Used by 1

Statement usesNormal clause detours · Hamiltonian paths · Deleting the clause vertices from a path · Arcs of the HAMPATH construction · Distinct variables of a formula · Row vertices counted from either end · Tops of the diamonds · CNF formula · CNF clause

Proof usesConsecutive vertices of the contracted path are joined by arcs · Every vertex of the contracted path except its end has a successor · Row vertices of a diamond · Row vertices lie below the next top · Out-neighbours of a row vertex outside the clause vertices · Tops are monotone in the diamond index · Tops of distinct diamonds are at least \(3m + 2\) apart · A Hamiltonian path visits every vertex · Entering a row and leaving it at once is impossible · Arcs of the PATH digraph

Used byBackward direction of SAT ≤ HAMPATH for paths with normal detours

TheoremEvery top but the last is followed by an end of its row#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables. In Sipser's HAMPATH graph for \(\varphi\), clause \(j\) is vertex \(j < m\), the top of diamond \(i\) is \(t_i = m + i(3m + 2)\), and vertex \(l \le 3m\) of its row is \(r_{i,l} = t_i + 1 + l\). Let \(p\) be a Hamiltonian path of this graph (on the vertices \(0, \dots, t_k\)) from \(t_0\) to \(t_k\) whose detours are normal: for every \(j < m\) there is \(i < k\) such that \(j\) sits in \(p\) immediately between \(r_{i,3j+1}\) and \(r_{i,3j+2}\), in either order. Let \(p'\) be \(p\) with the clause vertices deleted. Then for every \(i < k\), the top \(t_i\) is immediately followed in \(p'\) by \(r_{i,0}\) or by \(r_{i,3m}\).

theorem exists_top_succ {i : ℕ} (hi : i < (hamVars φ).length) (hd : DetoursNormal φ p) :
    ∃ b, [hpT φ.length i, hpRo φ.length i b 0] <:+: dropClauses φ p

Uses 17 · Used by 1

Statement usesNormal clause detours · Hamiltonian paths · Deleting the clause vertices from a path · Arcs of the HAMPATH construction · Distinct variables of a formula · Row vertices counted from either end · Tops of the diamonds · CNF formula · CNF clause

Proof usesConsecutive vertices of the contracted path are joined by arcs · Every vertex of the contracted path except its end has a successor · Row vertices of a diamond · Out-neighbours of a top · Tops are monotone in the diamond index · Tops of distinct diamonds are at least \(3m + 2\) apart · A Hamiltonian path visits every vertex · Arcs of the PATH digraph

Used byBackward direction of SAT ≤ HAMPATH for paths with normal detours

TheoremPositions in the list of distinct variables#✓fully proved

Let \(\varphi\) be a CNF formula, let \(v_0, \dots, v_{k-1}\) be the list of distinct variables of \(\varphi\), and let \(i < k\). Then the first position at which \(v_i\) occurs in this list is \(i\).

theorem idxOf_getD_hamVars {φ : CNF} {i : ℕ} (hi : i < (hamVars φ).length) :
    (hamVars φ).idxOf ((hamVars φ).getD i 0) = i

Uses 3 · Used by 1

Statement usesDistinct variables of a formula · CNF formula

Proof usesOccurrence list of a CNF formula

Used byBackward direction of SAT ≤ HAMPATH for paths with normal detours

TheoremBackward direction of SAT ≤ HAMPATH for paths with normal detours#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables. In Sipser's HAMPATH graph for \(\varphi\), clause \(j\) is vertex \(j < m\), the top of diamond \(i\) is \(t_i = m + i(3m + 2)\), and vertex \(l \le 3m\) of its row is \(r_{i,l} = t_i + 1 + l\). If \(p\) is a Hamiltonian path of this graph (on the vertices \(0, \dots, t_k\)) from \(t_0\) to \(t_k\) whose detours are normal, that is, for every \(j < m\) there is \(i < k\) such that \(j\) sits in \(p\) immediately between \(r_{i,3j+1}\) and \(r_{i,3j+2}\), in either order, then \(\varphi\) is satisfiable.

The satisfying assignment makes the variable of diamond \(i\) true iff row \(i\) is traversed from left to right.

theorem cnfSat_of_isHamPath {φ : CNF} {p : List ℕ}
    (h : IsHamPath (hpT φ.length (hamVars φ).length + 1) (hamEdges φ)
      (hpT φ.length 0) (hpT φ.length (hamVars φ).length) p)
    (hd : DetoursNormal φ p) : CNFSat φ

Uses 18 · Used by 1

Statement usesNormal clause detours · Hamiltonian paths · Arcs of the HAMPATH construction · Distinct variables of a formula · Tops of the diamonds · CNF formula · CNF clause · Satisfiability of a CNF formula

Proof usesDeleting the clause vertices from a path · Every top but the last is followed by an end of its row · Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs · Row vertices of a diamond · Arcs from a row into a clause vertex · Row vertices counted from either end · Positions in the list of distinct variables · Contracting a clause detour · A row entered at one end is run to the other end · Arcs of the PATH digraph

Used byThe construction has a Hamiltonian path iff the formula is satisfiable

TheoremThe construction has a Hamiltonian path iff the formula is satisfiable#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables, and let \(t_i = m + i(3m + 2)\) be the top vertex of diamond \(i\) in Sipser's construction. The digraph on the vertices \(0, \dots, t_k\) whose arcs are the arcs of the construction for \(\varphi\) has a Hamiltonian path from \(t_0\) to \(t_k\) if and only if \(\varphi\) is satisfiable.

theorem exists_isHamPath_iff_cnfSat (φ : CNF) :
    (∃ p, IsHamPath (hpT φ.length (hamVars φ).length + 1) (hamEdges φ)
      (hpT φ.length 0) (hpT φ.length (hamVars φ).length) p) ↔ CNFSat φ

Uses 10 · Used by 1

Statement usesHamiltonian paths · Arcs of the HAMPATH construction · Distinct variables of a formula · Tops of the diamonds · CNF formula · CNF clause · Satisfiability of a CNF formula

Proof usesBackward direction of SAT ≤ HAMPATH for paths with normal detours · Hamiltonian paths of Sipser's graph have normal detours · Satisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction)

Used bySAT ≤ HAMPATH preserves membership

TheoremHAMPATH on an encoded instance#✓fully proved

For all natural numbers \(s\), \(t\), \(n\) and every list \(E\) of pairs of natural numbers, the HAMPATH decision problem accepts the PATH encoding of \((s, t, n, E)\) if and only if the digraph on \(0, \dots, n - 1\) with edge list \(E\) has a Hamiltonian path from \(s\) to \(t\).

theorem hamPathDec_encodeP (s t n : ℕ) (es : List (ℕ × ℕ)) :
    hamPathDec (Path.encodeP s t n es) = true ↔ ∃ p, IsHamPath n es s t p

Uses 4 · Used by 2

Statement usesHamiltonian paths · The HAMPATH problem · Encoding of a PATH instance

Proof usesThe PATH instance encoding is injective

Used byHAMPATH rejects the fixed no-instance · SAT ≤ HAMPATH preserves membership

TheoremHAMPATH rejects the fixed no-instance#✓fully proved

The HAMPATH decision problem rejects the PATH encoding of the digraph on the two vertices \(0, 1\) with no arcs and \(s = t = 0\): a path from \(0\) to \(0\) that visits both vertices would repeat \(0\).

theorem hamPathDec_noHam : hamPathDec noHam = false

Uses 6 · Used by 1

Statement usesThe HAMPATH problem · A fixed HAMPATH no-instance

Proof usesHamiltonian paths · HAMPATH on an encoded instance · Arcs of the PATH digraph · Encoding of a PATH instance

Used bySAT ≤ HAMPATH preserves membership

TheoremSAT ≤ HAMPATH preserves membership#✓fully proved

For every bit string \(x\), SAT accepts \(x\) if and only if HAMPATH accepts the image of \(x\) under the SAT-to-HAMPATH reduction map.

theorem satDec_eq_hamPathDec_reduceHam (x : List Bool) : satDec x = hamPathDec (reduceHam x)

Uses 21 · Used by 1

Statement usesThe HAMPATH problem · The SAT-to-HAMPATH reduction map · SAT as a decision problem

Proof usesSAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · Hamiltonian paths · The construction has a Hamiltonian path iff the formula is satisfiable · Arcs of the HAMPATH construction · HAMPATH on an encoded instance · HAMPATH rejects the fixed no-instance · Distinct variables of a formula · Tops of the diamonds · A fixed HAMPATH no-instance · Sipser's HAMPATH instance of a CNF formula · Encoding of a PATH instance · Decoding a complete length-prefixed CNF formula · The CNF decoder inverts the length-prefixed CNF code · Length-prefixed binary code of a CNF formula · CNF formula · CNF clause · Satisfiability of a CNF formula

Used byHAMPATH is NP-hard

InductiveStacks of the Hamiltonian path verifier#✓fully proved

The verifier has twelve stacks: the input \(X\) and the witness \(W\); the counters \(S\), \(T\), \(N\) (holding \(s\), \(t\), \(n\)), \(C\) (the number of vertices seen), \(A\) (the current vertex) and \(B\) (the previous one); the save stacks \(E\) (for \(X\)) and \(Z\) (for \(W\)); and the scratch stacks \(R\) and \(Q\).

inductive K | X | W | S | T | N | C | A | B | E | Z | R | Q
  deriving DecidableEq

Used by 32

Used byFirst counter of a HAMPATH-verifier comparison · Second counter of a HAMPATH-verifier comparison · Step of the HAMPATH verifier's unary comparison loop · Emptiness test · The unary reader of the Hamiltonian path verifier · The unary mover of the Hamiltonian path verifier · Statements of the Hamiltonian-path verifier · Run of the HAMPATH verifier's unary comparison loop · Run of a HAMPATH-verifier counter comparison · HAMPATH-verifier unary comparison with the counter restored · One step of the emptiness test · Moving a stack of bits · The Hamiltonian path verifier machine · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The unary reader of the Hamiltonian path verifier reads a terminated number · The edge scan of the Hamiltonian path verifier · The unary mover of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier moves a terminated number · A single step of the Hamiltonian-path verifier · Interleaved stack updates in the Hamiltonian-path verifier · The edge-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier · HAMPATH is in NP · The HAMPATH verifier as a host component · Running the head-or-edge check · Stack layout between vertex steps · Running the vertex loop · Stack layout during a vertex step · The repeat scan of the Hamiltonian path verifier · Correctness and running time of the Hamiltonian path verifier · One vertex step of the Hamiltonian-path verifier · The rest of a vertex step in the Hamiltonian-path verifier

InductiveCounter comparisons of the HAMPATH verifier#✓fully proved

The four-element type of the comparisons the verifier makes between its counters: the current vertex \(a\) with the vertex count \(n\), the current vertex \(a\) with the start vertex \(s\), the number \(c\) of vertices seen with \(n\), and the previous vertex \(b\) with the end vertex \(t\).

inductive CI | an | as | cn | bt
  deriving DecidableEq

Used by 13

Used byFirst counter of a HAMPATH-verifier comparison · Second counter of a HAMPATH-verifier comparison · Labels of the Hamiltonian path verifier · Run of a HAMPATH-verifier counter comparison · Exit labels of the counter comparisons · Outcome of the HAMPATH verifier's vertex-range comparison · Outcome of a HAMPATH-verifier equality comparison · The Hamiltonian path verifier machine · HAMPATH is in NP · The HAMPATH verifier as a host component · Running the head-or-edge check · Running the vertex loop · One vertex step of the Hamiltonian-path verifier

InductiveLabels of the Hamiltonian path verifier#✓fully proved

The instruction labels of the verifier: reading \(s\), \(t\), \(n\); validating the edge list and putting it back; validating the witness and putting it back; the vertex loop, reading a vertex, and the head-or-edge dispatch; for each of the four counter comparisons, the comparison itself and, for each of its three outcomes, the two loops restoring the compared counters; the edge scan (comparing an edge's ends, with a flag for the verdict so far, restoring the counters, putting the edge list back); the repeat scan (likewise flagged comparisons and restores, then putting the witness back); the final nonzero-count check; counting the vertex and making it the previous one; accept; and reject.

inductive Lab
  | rdS | rdT | rdN | vE | vEU | vEV | vEb | vW | vWU | vWb | loop | rdA | hd
  | cmp (i : CI) | cr (i : CI) (o : Ordering) | crb (i : CI) (o : Ordering)
  | scan | ceU (ok : Bool) | rsU (ok : Bool) | ceV (ok : Bool) | rsV (ok : Bool) | scB
  | nd | cbN (ok : Bool) | rsN (ok : Bool) | ndB | fin | incC | dB | mA | yes | no
  deriving DecidableEq

Uses 1 · Used by 31

Statement usesCounter comparisons of the HAMPATH verifier

Used byStep of the HAMPATH verifier's unary comparison loop · Emptiness test · The unary reader of the Hamiltonian path verifier · The unary mover of the Hamiltonian path verifier · Statements of the Hamiltonian-path verifier · Run of the HAMPATH verifier's unary comparison loop · Run of a HAMPATH-verifier counter comparison · HAMPATH-verifier unary comparison with the counter restored · Exit labels of the counter comparisons · Outcome of the HAMPATH verifier's vertex-range comparison · Outcome of a HAMPATH-verifier equality comparison · One step of the emptiness test · Moving a stack of bits · The Hamiltonian path verifier machine · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The unary reader of the Hamiltonian path verifier reads a terminated number · The edge scan of the Hamiltonian path verifier · The unary mover of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier moves a terminated number · Start label of the Hamiltonian-path verifier · A single step of the Hamiltonian-path verifier · The edge-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier · HAMPATH is in NP · The HAMPATH verifier as a host component · Running the head-or-edge check · Running the vertex loop · The repeat scan of the Hamiltonian path verifier · Correctness and running time of the Hamiltonian path verifier · One vertex step of the Hamiltonian-path verifier · The rest of a vertex step in the Hamiltonian-path verifier

AbbreviationStatements of the Hamiltonian-path verifier#✓fully proved

A statement of the verifier is a statement of a multi-stack Turing machine whose stacks are indexed by the verifier's stacks \(K\), each stack over the alphabet \(\mathrm{Sym}\), with labels \(\mathrm{Lab}\) and a Boolean internal variable.

abbrev Stmt := TM2.Stmt (fun _ : K => Sym) Lab Bool

Uses 3 · Used by 4

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Stack alphabet of the SAT verifier

Used byStep of the HAMPATH verifier's unary comparison loop · Emptiness test · The unary reader of the Hamiltonian path verifier · The unary mover of the Hamiltonian path verifier

DefinitionThe unary reader of the Hamiltonian path verifier#✓fully proved

For stacks \(\mathsf{src}\) and \(c\) and labels \(\ell\) (its own) and \(m\) (the next one), the statement that goes to label \(\mathrm{no}\) if \(\mathsf{src}\) is empty; otherwise it pops the top symbol of \(\mathsf{src}\) and, if that symbol is the bit true, pushes the bit true (one unit) onto \(c\) and goes to \(\ell\), while if it is anything else it goes to \(m\). Each of the two tests also stores its outcome in the Boolean variable.

Run in a loop at \(\ell\), it reads a unary number off \(\mathsf{src}\) onto the counter \(c\) and consumes the terminator.

def readU (src c : K) (self next : Lab) : Stmt :=
  .peek src (fun _ o => o.isNone) <| .branch id (.goto fun _ => .no) <|
    .pop src (fun _ o => bitOf Sym.bit? o) <| .branch id
      (.push c (fun _ => .bit true) (.goto fun _ => self)) (.goto fun _ => next)

Uses 6 · Used by 3

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Statements of the Hamiltonian-path verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byThe Hamiltonian path verifier machine · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The unary reader of the Hamiltonian path verifier reads a terminated number

DefinitionThe unary mover of the Hamiltonian path verifier#✓fully proved

For stacks \(\mathsf{src}\) and \(\mathsf{dst}\) and labels \(\ell\) (its own) and \(m\) (the next one), the statement that goes to label \(\mathrm{no}\) if \(\mathsf{src}\) is empty; otherwise it pops the top symbol of \(\mathsf{src}\), reads it as the bit true if it is the bit true and as false otherwise, pushes that bit onto \(\mathsf{dst}\), and goes to \(\ell\) if the bit is true and to \(m\) if it is false. Each of the two tests also stores its outcome in the Boolean variable.

Run in a loop at \(\ell\), it moves a unary number, terminator included, from \(\mathsf{src}\) to \(\mathsf{dst}\).

def skipU (src dst : K) (self next : Lab) : Stmt :=
  .peek src (fun _ o => o.isNone) <| .branch id (.goto fun _ => .no) <|
    .pop src (fun _ o => bitOf Sym.bit? o) <| .push dst (fun b => .bit b) <| .branch id
      (.goto fun _ => self) (.goto fun _ => next)

Uses 6 · Used by 3

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Statements of the Hamiltonian-path verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byThe Hamiltonian path verifier machine · The unary mover of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier moves a terminated number

DefinitionEmptiness test#✓fully proved

For a stack \(k\) and labels \(e\) and \(ne\), the verifier instruction that looks at the top of stack \(k\) without changing any stack, then goes to \(e\) if \(k\) is empty and to \(ne\) otherwise.

def ifE (k : K) (e ne : Lab) : Stmt :=
  .peek k (fun _ o => o.isNone) <| .branch id (.goto fun _ => e) (.goto fun _ => ne)

Uses 4 · Used by 2

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Statements of the Hamiltonian-path verifier · Stack alphabet of the SAT verifier

Used byOne step of the emptiness test · The Hamiltonian path verifier machine

DefinitionStep of the HAMPATH verifier's unary comparison loop#✓fully proved

For stacks \(\mathit{src}\), \(\mathit{sv}\), \(c\) of the HAMPATH verifier, label families \(\mathit{self}\) and \(\mathit{fin}\) indexed by booleans, and a boolean verdict \(\mathit{ok}\), this is the instruction that pops the top of \(\mathit{src}\), reads it as a bit \(b\) (false if \(\mathit{src}\) is empty or its top is not a bit symbol), and pushes the bit symbol of \(b\) onto \(\mathit{sv}\). If \(b\) is true, it pops \(c\); if \(c\) was nonempty it pushes the bit symbol of true onto the scratch stack \(R\) and goes to \(\mathit{self}(\mathit{ok})\), and otherwise it goes to \(\mathit{self}(\mathrm{false})\). If \(b\) is false, it goes to \(\mathit{fin}(\mathit{ok})\) when \(c\) is empty and to \(\mathit{fin}(\mathrm{false})\) otherwise.

Iterated, it compares the next unary number of \(\mathit{src}\) with the counter \(c\), one unit of \(c\) per true, parked on \(R\): \(\mathit{ok}\) is the verdict so far, falsified when \(c\) runs out early.

def cbS (src sv c : K) (self fin : Bool → Lab) (ok : Bool) : Stmt :=
  .pop src (fun _ o => bitOf Sym.bit? o) <| .push sv (fun b => .bit b) <| .branch id
    (.pop c (fun _ o => o.isSome) <| .branch id
      (.push .R (fun _ => .bit true) (.goto fun _ => self ok)) (.goto fun _ => self false))
    (.peek c (fun _ o => o.isNone) <| .branch id (.goto fun _ => fin ok)
      (.goto fun _ => fin false))

Uses 6 · Used by 3

Statement usesStacks of the Hamiltonian path verifier · Labels of the Hamiltonian path verifier · Statements of the Hamiltonian-path verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byRun of the HAMPATH verifier's unary comparison loop · HAMPATH-verifier unary comparison with the counter restored · The Hamiltonian path verifier machine

DefinitionFirst counter of a HAMPATH-verifier comparison#✓fully proved

The function from the four counter comparisons of the HAMPATH verifier to its stacks that sends the comparisons of the current vertex with the vertex count and of the current vertex with the start vertex to the current-vertex counter \(A\), the comparison of the number of vertices seen with the vertex count to the vertices-seen counter \(C\), and the comparison of the previous vertex with the end vertex to the previous-vertex counter \(B\).

def ca : CI → K
  | .an => .A
  | .as => .A
  | .cn => .C
  | .bt => .B

Uses 2 · Used by 4

Statement usesCounter comparisons of the HAMPATH verifier · Stacks of the Hamiltonian path verifier

Used byRun of a HAMPATH-verifier counter comparison · The Hamiltonian path verifier machine · Running the head-or-edge check · One vertex step of the Hamiltonian-path verifier

DefinitionSecond counter of a HAMPATH-verifier comparison#✓fully proved

The function from the four counter comparisons of the HAMPATH verifier to its stacks that sends the comparisons of the current vertex with the vertex count and of the number of vertices seen with the vertex count to the vertex-count counter \(N\), the comparison of the current vertex with the start vertex to the start-vertex counter \(S\), and the comparison of the previous vertex with the end vertex to the end-vertex counter \(T\).

def cb : CI → K
  | .an => .N
  | .as => .S
  | .cn => .N
  | .bt => .T

Uses 2 · Used by 4

Statement usesCounter comparisons of the HAMPATH verifier · Stacks of the Hamiltonian path verifier

Used byRun of a HAMPATH-verifier counter comparison · The Hamiltonian path verifier machine · Running the head-or-edge check · One vertex step of the Hamiltonian-path verifier

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.