The row of a diamond in the HAMPATH emitter to A row starts at its left end

TheoremThe row 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 \(P = \tau\), \(M = 3m\), \(L = 0\), \(R = 0\), \(N \le B\), \(J \le B\) and \(D \le B\), and suppose \(\rho_{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) + 2B + 5\) steps, from label \(\mathsf{r0}\) 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 drowFull_run (Bd m dI : ℕ) (s : MS) (v : Bool) (hp : s.p = hpT m dI)
    (hmm : s.mm = 3 * m) (hl : s.l = 0) (hr : s.r = 0) (hn : s.n ≤ Bd) (hj : s.j ≤ Bd)
    (hd : s.d ≤ Bd) (hB : hpR m dI (3 * m) ≤ Bd) :
    ∃ v', RunLe prog (Bd * (8 * Bd + 15) + 2 * Bd + 5) ⟨some .r0, 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 17 · 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 · Tops of the diamonds · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesCopying a counter in the HAMPATH emitter · The row loop of a diamond in the HAMPATH emitter · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Unary counter

Used byOne diamond

TheoremThe detours of a diamond#✓fully proved

Let \(B, i, y \in \mathbb{N}\), let \(\varphi\) be a CNF formula with \(m\) clauses and token list \(\mathrm{toks}(\varphi)\), let \(\nu\) be a list of symbols and \(b\) a state bit, and let \(s\) be a quiescent state of the emitter such that \(F\) holds \(\mathrm{toks}(\varphi)\), \(T\) and the scratch stack \(X\) are empty, \(V\) holds the name of \(y\), then a clause separator, then \(\nu\), the counter \(P\) equals the top of diamond \(i\) for \(m\) clauses, the counters \(J\) and \(D\) are \(0\), the counters \(N\) and \(R\) are at most \(B\), the binary encoding of \(y\) has length at most \(B\), and row vertex \(3m\) of diamond \(i\) is at most \(B\). Then for some state bit \(b'\) the emitter goes in at most \(|\mathrm{toks}(\varphi)|(3B + 6) + m(16B + 26) + 2B + 5\) steps from label \(\mathrm{e0}\) with state bit \(b\) and the stacks of \(s\) to label \(\mathrm{t0}\) with state bit \(b'\) and the stacks of \(s\) changed as follows: \(F\) becomes empty, \(T\) becomes \(\mathrm{toks}(\varphi)\) reversed, \(J\) becomes \(m\), \(D\) becomes row vertex \(3m + 1\) of diamond \(i\), and the edge-bit list \(q\) is extended by the bits of the detour arcs, for \(j = 0, \dots, m - 1\) in order, of clause \(j\) of \(\varphi\) in diamond \(i\) for variable \(y\).

theorem ddet_run (Bd dI y : ℕ) (φ : CNF) (VR : List Sym) (s : MS) (v : Bool)
    (hf : s.f = toks φ) (ht : s.t = []) (hv : s.v = name y ++ Sym.cl :: VR) (hx : s.x = [])
    (hp : s.p = hpT φ.length dI) (hj : s.j = 0) (hd : s.d = 0) (hn : s.n ≤ Bd) (hr : s.r ≤ Bd)
    (hy : (encodeNat y).length ≤ Bd) (hB : hpR φ.length dI (3 * φ.length) ≤ Bd) :
    ∃ v', RunLe prog ((toks φ).length * (3 * Bd + 6) + φ.length * (16 * Bd + 26) + 2 * Bd + 5)
      ⟨some .e0, v, s.stk⟩
      ⟨some .t0, v', { s with
        f := [], t := (toks φ).reverse, j := φ.length, d := hpR φ.length dI (3 * φ.length + 1),
        q := s.q ++ Karp.edgeBits ((List.range φ.length).flatMap
          (fun j => detE φ.length dI y j (φ.getD j []))) }.stk⟩

Uses 23 · 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 · Tops of the diamonds · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · CNF clause · Runs within a step budget

Proof usesCopying a counter in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · Tokens of a clause · 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 byOne diamond

TheoremEnd of a diamond#✓fully proved

Let \(\varphi\) be a CNF formula with token list \(\mathrm{toks}(\varphi)\), let \(y \in \mathbb{N}\) have binary encoding \(\mathrm{bin}(y)\), let \(\nu\) be a list of symbols and \(b\) a state bit, and let \(s\) be a quiescent state of the emitter whose stack \(T\) holds \(\mathrm{toks}(\varphi)\) reversed, whose stack \(F\) is empty, and whose stack \(V\) holds the name of \(y\), then a clause separator, then \(\nu\). Let \(p, n, r, j, d\) be the values of the counters \(P, N, R, J, D\) of \(s\). Then for some state bit \(b'\) the emitter goes in exactly \(|\mathrm{toks}(\varphi)| + |\mathrm{bin}(y)| + n + p + r + j + d + 9\) steps from label \(\mathrm{t0}\) with state bit \(b\) and the stacks of \(s\) to label \(\mathrm{h0}\) with state bit \(b'\) and the stacks of the quiescent state obtained from \(s\) by emptying \(T\), setting \(F\) to \(\mathrm{toks}(\varphi)\) and \(V\) to \(\nu\), prepending the reversed name of \(y\) to \(G\), setting \(P\) to \(n + 1\), and setting \(N\), \(R\), \(J\) and \(D\) to \(0\).

theorem dback_run (φ : CNF) (y : ℕ) (VR : List Sym) (s : MS) (v : Bool)
    (ht : s.t = (toks φ).reverse) (hf : s.f = []) (hv : s.v = name y ++ Sym.cl :: VR) :
    ∃ v', Run prog ((toks φ).length + (encodeNat y).length + s.n + s.p + s.r + s.j + s.d + 9)
      ⟨some .t0, v, s.stk⟩
      ⟨some .h0, v', { s with
        t := [], f := toks φ, v := VR, g := (name y).reverse ++ s.g, p := s.n + 1, n := 0,
        r := 0, j := 0, d := 0 }.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 · Name of a variable in 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 · Exact-length runs of a TM2 machine

Proof usesDraining a counter · Token symbols of the HAMPATH emitter · Moving the tokens back in the HAMPATH emitter · Reading a symbol as a name bit · Tokens of a clause · Tokens of a literal · CNF clause · Flag bit of a machine state · Bit blocks · A single step executes the statement at the current label · Adding units to target stacks · Unary counter · Running the bit-moving loop · Running a counter transfer

Used byOne diamond

TheoremOne diamond#✓fully proved

Let \(B, i, y \in \mathbb{N}\), let \(u\) be a list of natural numbers, let \(\varphi\) be a CNF formula with \(m\) clauses and token list \(\mathrm{toks}(\varphi)\), let \(b\) be a state bit, and let \(s\) be a quiescent state of the emitter such that \(T\) and the scratch stack \(X\) are empty, \(F\) holds \(\mathrm{toks}(\varphi)\), \(V\) is the variable stack of the list \(y\) followed by \(u\), the counter \(P\) equals the top of diamond \(i\) for \(m\) clauses, the counter \(M\) equals \(3m\), the counters \(N, R, L, J, D\) are \(0\), and \(B\) bounds the top of diamond \(i + 1\), the length of the binary encoding of \(y\), and the length of \(\mathrm{toks}(\varphi)\). Then for some state bit \(b'\) the emitter goes in at most \(30B^2 + 100B + 100\) steps from label \(\mathrm{h0}\) with state bit \(b\) and the stacks of \(s\) back to label \(\mathrm{h0}\) with state bit \(b'\) and the stacks of \(s\) changed as follows: \(V\) becomes the variable stack of \(u\), \(P\) becomes the top of diamond \(i + 1\), the edge-bit list \(q\) is extended by the bits of the arcs of diamond \(i\) of \(\varphi\) for variable \(y\), and the reversed name of \(y\) is prepended to \(G\).

theorem diamond_run (Bd : ℕ) (φ : CNF) (dI y : ℕ) (ys : List ℕ) (s : MS) (v : Bool)
    (ht : s.t = []) (hf : s.f = toks φ) (hv : s.v = vstk (y :: ys)) (hx : s.x = [])
    (hp : s.p = hpT φ.length dI) (hmm : s.mm = 3 * φ.length) (hn : s.n = 0) (hr : s.r = 0)
    (hl : s.l = 0) (hj : s.j = 0) (hd : s.d = 0) (hBd : hpT φ.length (dI + 1) ≤ Bd)
    (hy : (encodeNat y).length ≤ Bd) (hL : (toks φ).length ≤ Bd) :
    ∃ v', RunLe prog (30 * Bd * Bd + 100 * Bd + 100) ⟨some .h0, v, s.stk⟩
      ⟨some .h0, v', { s with
        v := vstk ys, p := hpT φ.length (dI + 1), q := s.q ++ Karp.edgeBits (diamondEdges φ dI y),
        g := (name y).reverse ++ s.g }.stk⟩

Uses 30 · 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 · Variable stack of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · Arcs of a variable diamond · Bit encoding of an edge list · Tops of the diamonds · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · CNF clause · Runs within a step budget

Proof usesEnd of a diamond · The detours of a diamond · Clause detours in a diamond · Front of a diamond · The row of a diamond in the HAMPATH emitter · The frame of a diamond · Consecutive row vertices · The next diamond top follows the row · The row arcs of a diamond · Bits of concatenated edge lists · Row vertices of a diamond · Tokens of a clause · Tokens of a literal · Exact-length runs of a TM2 machine

Used byThe diamonds

TheoremThe diamonds#✓fully proved

Let \(B \in \mathbb{N}\) and let \(\varphi\) be a CNF formula with \(m\) clauses, token list \(\mathrm{toks}(\varphi)\) and list of distinct variables \(\mathrm{vars}(\varphi)\) of length \(k\). Suppose the top of diamond \(k\) for \(m\) clauses, the length of \(\mathrm{toks}(\varphi)\), and the length of the binary encoding of every \(y \in \mathrm{vars}(\varphi)\) are at most \(B\). Let \(\mathrm{vars}(\varphi)\) split as a list \(\pi\) followed by a list \(u\), let \(b\) be a state bit, and let \(s\) be a quiescent state of the emitter such that \(T\) and the scratch stack \(X\) are empty, \(F\) holds \(\mathrm{toks}(\varphi)\), \(V\) is the variable stack of \(u\), the counter \(P\) equals the top of diamond \(|\pi|\), the counter \(M\) equals \(3m\), the counters \(N, R, L, J, D\) are \(0\), and the edge-bit list \(q\) is the bits of the arcs of diamonds \(0, \dots, |\pi| - 1\) in order, diamond \(i\) taken for the \(i\)-th entry of \(\mathrm{vars}(\varphi)\). Then for some state bit \(b'\) and some stack contents \(g'\) the emitter goes in at most \(|u|(30B^2 + 100B + 100)\) steps from label \(\mathrm{h0}\) with state bit \(b\) and the stacks of \(s\) back to label \(\mathrm{h0}\) with state bit \(b'\) and the stacks of \(s\) changed as follows: \(V\) becomes empty, \(P\) becomes the top of diamond \(k\), \(q\) becomes the bits of all arcs of the construction for \(\varphi\), and \(G\) becomes \(g'\).

theorem diamonds_run (Bd : ℕ) (φ : CNF) (hBd : hpT φ.length (hamVars φ).length ≤ Bd)
    (hL : (toks φ).length ≤ Bd) (hnm : ∀ y ∈ hamVars φ, (encodeNat y).length ≤ Bd) :
    ∀ (ys pre : List ℕ), hamVars φ = pre ++ ys → ∀ (s : MS) (v : Bool), s.t = [] →
      s.f = toks φ → s.v = vstk ys → s.x = [] → s.p = hpT φ.length pre.length →
      s.mm = 3 * φ.length → s.n = 0 → s.r = 0 → s.l = 0 → s.j = 0 → s.d = 0 →
      s.q = Karp.edgeBits ((List.range pre.length).flatMap
        (fun i => diamondEdges φ i ((hamVars φ).getD i 0))) →
      ∃ v' g', RunLe prog (ys.length * (30 * Bd * Bd + 100 * Bd + 100)) ⟨some .h0, v, s.stk⟩
        ⟨some .h0, v', { s with
          v := [], p := hpT φ.length (hamVars φ).length, q := Karp.edgeBits (hamEdges φ),
          g := g' }.stk⟩

Uses 22 · 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 · Variable stack of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · Arcs of a variable diamond · Bit encoding of an edge list · Arcs of the HAMPATH construction · Distinct variables of a formula · Tops of the diamonds · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · CNF clause · Runs within a step budget

Proof usesOne diamond · Name of a variable in the HAMPATH emitter · Bits of concatenated edge lists · Tops are monotone in the diamond index · Exact-length runs of a TM2 machine

Used byCorrectness and running time of the HAMPATH emitter

TheoremThe output phase of the HAMPATH emitter#✓fully proved

Let \(s\) be a quiescent state of the emitter whose variable stack \(V\) is empty, with clause count \(C = c\), diamond-top counter \(P = p\), edge bits \(q\) and output stack \(o\). Then for every internal bit \(v\) there are an internal bit \(v'\) and stacks \(S'\) such that the emitter goes in exactly \(|q| + 4p + 2c + 11\) steps from label \(\mathsf{h0}\) with bit \(v\) and the stacks of \(s\) to label \(\mathsf{done}\) with bit \(v'\) and stacks \(S'\), and the output stack of \(S'\) is \(1^c 0 1^p 0 1^{p+1} 0\) followed by \(q\) and then \(o\).

theorem final_run (s : MS) (v : Bool) (hv : s.v = []) :
    ∃ v' S', Run prog (s.q.length + 4 * s.p + 2 * s.c + 11) ⟨some .h0, v, s.stk⟩
      ⟨some .done, v', S'⟩ ∧ S' .O = List.replicate s.c true ++ false ::
        (List.replicate s.p true ++ false :: (List.replicate (s.p + 1) true ++ false ::
          (s.q ++ s.o)))

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 · The HAMPATH emitter machine · Stack alphabets of the HAMPATH emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesCopying a counter in the HAMPATH emitter · Reading a symbol as a name bit · Flag bit of a machine state · Bit blocks · A single step executes the statement at the current label · Unary counter · Running the bit-moving loop · Pushing a list of symbols onto one stack

Used byCorrectness and running time of the HAMPATH emitter

TheoremCorrectness and running time of the HAMPATH emitter#✓fully proved

Let \(\varphi\) be a CNF formula with token sequence \(\mathrm{toks}(\varphi)\), let \(o\) be a list of bits, and let \(S\) be stacks in which the token stack \(T\) holds \(\mathrm{toks}(\varphi)\) reversed, the output stack \(O\) holds \(o\), and every other stack is empty. Then for every internal bit \(v\) there are an internal bit \(v'\) and stacks \(S'\) such that the emitter goes, in at most \(2000(|\mathrm{toks}(\varphi)| + 1)^5\) steps, from its start label with bit \(v\) and stacks \(S\) to label \(\mathsf{done}\) with bit \(v'\) and stacks \(S'\), and the output stack of \(S'\) is Sipser's HAMPATH instance for \(\varphi\) followed by \(o\) (so the instance is read top-first).

theorem run (φ : CNF) (o : List Bool) (v : Bool) (St : ∀ k, List (Γ k))
    (hT : St .T = (toks φ).reverse) (hO : St .O = o) (h0 : ∀ k, k ≠ .T → k ≠ .O → St k = []) :
    ∃ v' S', RunLe prog (2000 * ((toks φ).length + 1) ^ 5) ⟨some start, v, St⟩
      ⟨some .done, v', S'⟩ ∧ S' .O = toHam φ ++ o

Uses 35 · Used by 1

Statement usesStacks of the HAMPATH emitter · Labels of the HAMPATH emitter · The HAMPATH emitter machine · Start label of the HAMPATH emitter · Stack alphabets of the HAMPATH emitter · Sipser's HAMPATH instance of a CNF formula · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · Runs within a step budget

Proof usesQuiescent states of the HAMPATH emitter · Stacks of a quiescent emitter state · Clause detours in a diamond · The emitter state before the diamonds · The diamonds · Length bound for the bit encoding of an edge list · The output phase of the HAMPATH emitter · The frame of a diamond · The next diamond top follows the row · Initial state of the HAMPATH emitter · Phase A of the HAMPATH emitter · The row arcs of a diamond · The HAMPATH instance as unary blocks and arc bits · Arcs of a variable diamond · Bit encoding of an edge list · Arcs of the HAMPATH construction · Distinct variables of a formula · Row vertices of a diamond · Tops of the diamonds · Tops are monotone in the diamond index · Tokens of a clause · Tokens of a literal · Occurrence list of a CNF formula · CNF clause · Exact-length runs of a TM2 machine

Used byThe HAMPATH emitter

DefinitionThe row of a diamond with its clauses inserted#✓fully proved

Let \(m\) and \(i\) be natural numbers and \(c : \mathbb{N} \to \mathbb{N}\) a map, and write \(r_l = m + i(3m + 2) + 1 + l\) for the row vertices of diamond \(i\). The row of diamond \(i\) for \(c\) is the list \(r_0, r_1, \dots, r_{3m}\) in which, for every \(j < m\) with \(c(j) = i\), the clause vertex \(j\) is inserted right after \(r_{3j+1}\).

def hfRow (m i : ℕ) (c : ℕ → ℕ) : List ℕ :=
  (List.range (3 * m + 1)).flatMap fun l =>
    hpR m i l :: if l % 3 = 1 ∧ c (l / 3) = i then [l / 3] else []

Uses 1 · Used by 8

Statement usesRow vertices of a diamond

Used byA row starts at its left end · The visit of a diamond · A diamond visit is a block of consecutive vertices plus its clauses · The vertices of a diamond row · Chain condition for a diamond row · A row ends at its right end · The forward path starts at the first top · Chain condition for a diamond traversal

DefinitionClauses picked up by a diamond#✓fully proved

For natural numbers \(m\) and \(i\) and a map \(c : \mathbb{N} \to \mathbb{N}\), the clauses picked up by diamond \(i\) are the list of all \(j < m\) with \(c(j) = i\), in increasing order.

These are the clause vertices of the row of diamond \(i\), in row order.

def hfPicks (m i : ℕ) (c : ℕ → ℕ) : List ℕ :=
  (List.range (3 * m + 1)).flatMap fun l => if l % 3 = 1 ∧ c (l / 3) = i then [l / 3] else []

Used by 6

Used byEach clause is picked up by exactly one row · A diamond visit is a block of consecutive vertices plus its clauses · The forward path visits every vertex once · The vertices of a diamond row · Clause vertices picked up by a row · The clause vertices of a row are distinct

DefinitionThe visit of a diamond#✓fully proved

For \(m\) clauses, a diamond \(i\), a clause-to-diamond map \(c\) and a direction \(b\), the visit of diamond \(i\) is the list consisting of its top \(T_i = m + i(3m+2)\) followed by its row with the clauses sent to \(i\) by \(c\) inserted, read left to right if \(b\) is true and right to left otherwise.

def hfDiamond (m i : ℕ) (c : ℕ → ℕ) (b : Bool) : List ℕ :=
  hpT m i :: if b then hfRow m i c else (hfRow m i c).reverse

Uses 2 · Used by 8

Statement usesThe row of a diamond with its clauses inserted · Tops of the diamonds

Used byA diamond visit is a block of consecutive vertices plus its clauses · The forward path through the diamonds · The forward path visits every vertex once · The forward path ends at the last top · The forward path starts at the first top · Chain condition for a diamond traversal · Chain condition for the forward path · A satisfying choice gives a Hamiltonian path

DefinitionThe forward path through the diamonds#✓fully proved

Let \(m\) and \(k\) be natural numbers, let \(c : \mathbb{N} \to \mathbb{N}\) be a map and let \(d : \mathbb{N} \to \{\mathrm{true}, \mathrm{false}\}\) give each diamond \(i\) a direction \(d(i)\). The forward path through the first \(k\) diamonds is the list obtained by concatenating, for \(i = 0, 1, \dots, k - 1\) in this order, the traversal of diamond \(i\) for \(c\) in direction \(d(i)\), and then appending the vertex \(m + k(3m + 2)\), the top of diamond \(k\). Here the traversal of diamond \(i\) is its top \(m + i(3m + 2)\) followed by its row \(r_0, r_1, \dots, r_{3m}\), where \(r_l = m + i(3m + 2) + 1 + l\) and the clause vertex \(j\) is inserted right after \(r_{3j+1}\) for every \(j < m\) with \(c(j) = i\); the row is read left to right if \(d(i)\) is true and right to left otherwise.

def hfPath (m k : ℕ) (c : ℕ → ℕ) (d : ℕ → Bool) : List ℕ :=
  (List.range k).flatMap (fun i => hfDiamond m i c (d i)) ++ [hpT m k]

Uses 2 · Used by 6

Statement usesThe visit of a diamond · Tops of the diamonds

Used byThe forward path visits every vertex once · Satisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction) · The forward path ends at the last top · The forward path starts at the first top · Chain condition for the forward path · A satisfying choice gives a Hamiltonian path

TheoremClause vertices picked up by a row#✓fully proved

Let \(m\) and \(i\) be natural numbers and let \(c : \mathbb{N} \to \mathbb{N}\). A natural number \(v\) is one of the clause vertices picked up by the row of diamond \(i\) under \(c\), for \(m\) clauses, if and only if \(v < m\) and \(c(v) = i\).

theorem mem_hfPicks {m i v : ℕ} {c : ℕ → ℕ} : v ∈ hfPicks m i c ↔ v < m ∧ c v = i

Uses 1 · Used by 1

Statement usesClauses picked up by a diamond

Used byEach clause is picked up by exactly one row

TheoremThe clause vertices of a row are distinct#✓fully proved

For all natural numbers \(m\), \(i\) and every function \(c : \mathbb{N} \to \mathbb{N}\), the list of clause vertices picked up by the row of diamond \(i\) under \(c\), for \(m\) clauses, has no repeated entries.

theorem nodup_hfPicks (m i : ℕ) (c : ℕ → ℕ) : (hfPicks m i c).Nodup

Uses 1 · Used by 1

Statement usesClauses picked up by a diamond

Used byEach clause is picked up by exactly one row

TheoremEach clause is picked up by exactly one row#✓fully proved

Let \(m, k\) be natural numbers and let \(c\) send every clause \(j < m\) to a diamond \(c(j) < k\). For each diamond \(i\), list the clauses \(j < m\) with \(c(j) = i\) in increasing order (the clause vertices picked up by the row of diamond \(i\)). Concatenating these lists for \(i = 0, \dots, k - 1\) gives a permutation of \(0, 1, \dots, m - 1\).

theorem flatMap_hfPicks_perm {m k : ℕ} {c : ℕ → ℕ} (hc : ∀ j < m, c j < k) :
    (List.range k).flatMap (fun i => hfPicks m i c) ~ List.range m

Uses 3 · Used by 1

Statement usesClauses picked up by a diamond

Proof usesClause vertices picked up by a row · The clause vertices of a row are distinct

Used byThe forward path visits every vertex once

TheoremThe vertices of a diamond row#✓fully proved

For natural numbers \(m\) and \(i\) and a map \(c : \mathbb{N} \to \mathbb{N}\), let \(r = m + i(3m + 2) + 1\) be the left end of the row of diamond \(i\). The row of diamond \(i\) for \(c\) (with its clause vertices inserted) is a permutation of the concatenation of the list \(r, r + 1, \dots, r + 3m\) and the list of clauses picked up by diamond \(i\) for \(c\), that is, of all \(j < m\) with \(c(j) = i\) in increasing order.

theorem hfRow_perm (m i : ℕ) (c : ℕ → ℕ) :
    hfRow m i c ~ List.range' (hpR m i 0) (3 * m + 1) ++ hfPicks m i c

Uses 3 · Used by 1

Statement usesClauses picked up by a diamond · The row of a diamond with its clauses inserted · Row vertices of a diamond

Used byA diamond visit is a block of consecutive vertices plus its clauses

TheoremA diamond visit is a block of consecutive vertices plus its clauses#✓fully proved

For \(m\) clauses, a diamond \(i\), a clause-to-diamond map \(c\) and a direction \(b\), let \(T_i = m + i(3m+2)\) be the top of diamond \(i\). The visit of diamond \(i\) in direction \(b\) is a rearrangement of the list that consists of \(T_i, T_i + 1, \dots, T_i + 3m + 1\) and then the clauses \(j < m\) with \(c(j) = i\) in increasing order.

theorem hfDiamond_perm (m i : ℕ) (c : ℕ → ℕ) (b : Bool) :
    hfDiamond m i c b ~ List.range' (hpT m i) (3 * m + 2) ++ hfPicks m i c

Uses 6 · Used by 1

Statement usesThe visit of a diamond · Clauses picked up by a diamond · Tops of the diamonds

Proof usesThe row of a diamond with its clauses inserted · The vertices of a diamond row · Row vertices of a diamond

Used byThe forward path visits every vertex once

TheoremThe first \(t\) diamonds occupy consecutive vertices#✓fully proved

For natural numbers \(m\) and \(t\), let \(T_i = m + i(3m+2)\). Concatenating, for \(i = 0, \dots, t - 1\), the lists \(T_i, T_i + 1, \dots, T_i + 3m + 1\) of \(3m + 2\) consecutive numbers (the top and the row of diamond \(i\)) gives the list \(m, m + 1, \dots, m + t(3m+2) - 1\), that is, the numbers from \(m\) to \(T_t - 1\) in increasing order.

theorem flatMap_range'_hpT (m t : ℕ) :
    (List.range t).flatMap (fun i => List.range' (hpT m i) (3 * m + 2)) =
      List.range' m (t * (3 * m + 2))

Uses 1 · Used by 1

Statement usesTops of the diamonds

Used byThe forward path visits every vertex once

TheoremThe forward path visits every vertex once#✓fully proved

Let \(m, k\) be natural numbers, let \(c\) send every clause \(j < m\) to a diamond \(c(j) < k\), let \(d\) be any directions, and let \(T_k = m + k(3m+2)\). The forward path through the first \(k\) diamonds in directions \(d\) with clause choice \(c\) is a permutation of the list \(0, 1, \dots, T_k\).

theorem hfPath_perm {m k : ℕ} {c : ℕ → ℕ} (d : ℕ → Bool) (hc : ∀ j < m, c j < k) :
    hfPath m k c d ~ List.range (hpT m k + 1)

Uses 7 · Used by 1

Statement usesThe forward path through the diamonds · Tops of the diamonds

Proof usesEach clause is picked up by exactly one row · The first \(t\) diamonds occupy consecutive vertices · The visit of a diamond · A diamond visit is a block of consecutive vertices plus its clauses · Clauses picked up by a diamond

Used byA satisfying choice gives a Hamiltonian path

TheoremChain condition for a diamond row#✓fully proved

Let \(R\) be a relation on \(\mathbb{N}\), let \(m\) and \(i\) be natural numbers and \(c : \mathbb{N} \to \mathbb{N}\) a map, and write \(r_l = m + i(3m + 2) + 1 + l\) for the row vertices of diamond \(i\). If \(R(r_l, r_{l+1})\) holds for every \(l < 3m\), and \(R(r_{3j+1}, j)\) and \(R(j, r_{3j+2})\) hold for every \(j < m\) with \(c(j) = i\), then the row of diamond \(i\) for \(c\) is a chain for \(R\): every entry is related by \(R\) to the next one.

theorem isChain_hfRow {R : ℕ → ℕ → Prop} {m i : ℕ} {c : ℕ → ℕ}
    (hrow : ∀ l < 3 * m, R (hpR m i l) (hpR m i (l + 1)))
    (hdet : ∀ j < m, c j = i → R (hpR m i (3 * j + 1)) j ∧ R j (hpR m i (3 * j + 2))) :
    (hfRow m i c).IsChain R

Uses 2 · Used by 1

Statement usesThe row of a diamond with its clauses inserted · Row vertices of a diamond

Used byChain condition for a diamond traversal

TheoremA row starts at its left end#✓fully proved

For \(m\) clauses, a diamond \(i\) and any clause-to-diamond map \(c\), the row of diamond \(i\) read left to right, with the clauses sent to \(i\) by \(c\) inserted, starts at its left end, the row vertex \(T_i + 1\), where \(T_i = m + i(3m+2)\) is the top of diamond \(i\).

theorem head?_hfRow (m i : ℕ) (c : ℕ → ℕ) : (hfRow m i c).head? = some (hpR m i 0)

Uses 2 · Used by 1

Statement usesThe row of a diamond with its clauses inserted · Row vertices of a diamond

Used byChain condition for a diamond traversal

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.