A row ends at its right end to Consecutive vertices of the contracted path are joined by arcs

TheoremA row ends at its right 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, ends at the row vertex \(T_i + 1 + 3m\), where \(T_i = m + i(3m+2)\) is the top of diamond \(i\).

theorem getLast?_hfRow (m i : ℕ) (c : ℕ → ℕ) :
    (hfRow m i c).getLast? = some (hpR m i (3 * m))

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

TheoremChain condition for a diamond traversal#✓fully proved

Let \(R\) be a relation on \(\mathbb{N}\), let \(m\) and \(i\) be natural numbers, \(c : \mathbb{N} \to \mathbb{N}\) a map and \(b\) a boolean, and write \(t_a = m + a(3m + 2)\) for the top of diamond \(a\) and \(r_l = t_i + 1 + l\) for the row vertices of diamond \(i\). Suppose that \(R(t_i, r_0)\), \(R(t_i, r_{3m})\), \(R(r_0, t_{i+1})\) and \(R(r_{3m}, t_{i+1})\) hold; that \(R(r_l, r_{l+1})\) and \(R(r_{l+1}, r_l)\) hold for every \(l < 3m\); that if \(b\) is true, then \(R(r_{3j+1}, j)\) and \(R(j, r_{3j+2})\) hold for every \(j < m\) with \(c(j) = i\); and that if \(b\) is false, then \(R(r_{3j+2}, j)\) and \(R(j, r_{3j+1})\) hold for every \(j < m\) with \(c(j) = i\). Then the traversal of diamond \(i\) for \(c\) in direction \(b\), followed by \(t_{i+1}\), is a chain for \(R\): every entry is related by \(R\) to the next one.

theorem isChain_hfDiamond {R : ℕ → ℕ → Prop} {m i : ℕ} {c : ℕ → ℕ} {b : Bool}
    (hT0 : R (hpT m i) (hpR m i 0)) (hT3 : R (hpT m i) (hpR m i (3 * m)))
    (hB0 : R (hpR m i 0) (hpT m (i + 1))) (hB3 : R (hpR m i (3 * m)) (hpT m (i + 1)))
    (hrow : ∀ l < 3 * m, R (hpR m i l) (hpR m i (l + 1)) ∧ R (hpR m i (l + 1)) (hpR m i l))
    (hpos : b = true → ∀ j < m, c j = i →
      R (hpR m i (3 * j + 1)) j ∧ R j (hpR m i (3 * j + 2)))
    (hneg : b = false → ∀ j < m, c j = i →
      R (hpR m i (3 * j + 2)) j ∧ R j (hpR m i (3 * j + 1))) :
    (hfDiamond m i c b ++ [hpT m (i + 1)]).IsChain R

Uses 7 · Used by 1

Statement usesThe visit of a diamond · Row vertices of a diamond · Tops of the diamonds

Proof usesA row ends at its right end · A row starts at its left end · The row of a diamond with its clauses inserted · Chain condition for a diamond row

Used byA satisfying choice gives a Hamiltonian path

TheoremChain condition for the forward path#✓fully proved

Let \(R\) be a relation on \(\mathbb{N}\), let \(m\) and \(k\) be natural numbers, \(c : \mathbb{N} \to \mathbb{N}\) a map and \(d : \mathbb{N} \to \{\mathrm{true}, \mathrm{false}\}\) a choice of directions, and write \(t_a = m + a(3m + 2)\) for the top of diamond \(a\). If for every \(i < k\) the traversal of diamond \(i\) for \(c\) in direction \(d(i)\), followed by \(t_{i+1}\), is a chain for \(R\) (every entry is related by \(R\) to the next one), then the forward path through the first \(k\) diamonds for \(c\) and \(d\) is a chain for \(R\).

theorem isChain_hfPath {R : ℕ → ℕ → Prop} {m k : ℕ} {c : ℕ → ℕ} {d : ℕ → Bool}
    (hD : ∀ i < k, (hfDiamond m i c (d i) ++ [hpT m (i + 1)]).IsChain R) :
    (hfPath m k c d).IsChain R

Uses 3 · Used by 1

Statement usesThe visit of a diamond · The forward path through the diamonds · Tops of the diamonds

Used byA satisfying choice gives a Hamiltonian path

TheoremThe forward path starts at the first top#✓fully proved

For \(m\) clauses, \(k\) diamonds, any clause-to-diamond map \(c\) and any directions \(d\), the forward path through the first \(k\) diamonds in directions \(d\) with clause choice \(c\) starts at the top \(T_0 = m\) of diamond \(0\).

theorem head?_hfPath (m k : ℕ) (c : ℕ → ℕ) (d : ℕ → Bool) :
    (hfPath m k c d).head? = some (hpT m 0)

Uses 4 · Used by 1

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

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

Used byA satisfying choice gives a Hamiltonian path

TheoremThe forward path ends at the last top#✓fully proved

For \(m\) clauses, \(k\) diamonds, any clause-to-diamond map \(c\) and any directions \(d\), the forward path through the first \(k\) diamonds in directions \(d\) with clause choice \(c\) ends at the top \(T_k = m + k(3m+2)\).

theorem getLast?_hfPath (m k : ℕ) (c : ℕ → ℕ) (d : ℕ → Bool) :
    (hfPath m k c d).getLast? = some (hpT m k)

Uses 3 · Used by 1

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

Proof usesThe visit of a diamond

Used byA satisfying choice gives a Hamiltonian path

TheoremDiamond arcs are arcs of the construction#✓fully proved

Let \(\varphi\) be a CNF formula, let \(x_0, \dots, x_{k-1}\) be its distinct variables in the order used by the construction, and let \(i < k\). Every arc of diamond \(i\) for variable \(x_i\) is an arc of the HAMPATH construction for \(\varphi\).

theorem mem_hamEdges_of_mem_diamondEdges {φ : CNF} {e : ℕ × ℕ} {i : ℕ} (hi : i < (hamVars φ).length)
    (h : e ∈ diamondEdges φ i ((hamVars φ).getD i 0)) : e ∈ hamEdges φ

Uses 4 · Used by 1

Statement usesArcs of a variable diamond · Arcs of the HAMPATH construction · Distinct variables of a formula · CNF formula

Used byA satisfying choice gives a Hamiltonian path

TheoremThe frame arcs of a diamond#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses, let \(i\) and \(x\) be natural numbers, and write \(t_a = m + a(3m + 2)\) for the top of diamond \(a\) and \(r_l = t_i + 1 + l\) for the row vertices of diamond \(i\). The four arcs \((t_i, r_0)\), \((t_i, r_{3m})\), \((r_0, t_{i+1})\) and \((r_{3m}, t_{i+1})\) are arcs of diamond \(i\) for the variable \(x\) in the construction for \(\varphi\).

theorem mem_diamondEdges_frame (φ : CNF) (i x : ℕ) :
    (hpT φ.length i, hpR φ.length i 0) ∈ diamondEdges φ i x ∧
      (hpT φ.length i, hpR φ.length i (3 * φ.length)) ∈ diamondEdges φ i x ∧
      (hpR φ.length i 0, hpT φ.length (i + 1)) ∈ diamondEdges φ i x ∧
      (hpR φ.length i (3 * φ.length), hpT φ.length (i + 1)) ∈ diamondEdges φ i x

Uses 5 · Used by 1

Statement usesArcs of a variable diamond · Row vertices of a diamond · Tops of the diamonds · CNF formula · CNF clause

Used byA satisfying choice gives a Hamiltonian path

TheoremRow arcs of a diamond#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses, let \(i\) and \(x\) be natural numbers, and write \(r_i(l)\) for row vertex \(l\) of diamond \(i\). For every \(l < 3m\), the arcs of diamond \(i\) for variable \(x\) include both the arc from \(r_i(l)\) to \(r_i(l+1)\) and the arc from \(r_i(l+1)\) to \(r_i(l)\).

theorem mem_diamondEdges_row (φ : CNF) (i x : ℕ) {l : ℕ} (hl : l < 3 * φ.length) :
    (hpR φ.length i l, hpR φ.length i (l + 1)) ∈ diamondEdges φ i x ∧
      (hpR φ.length i (l + 1), hpR φ.length i l) ∈ diamondEdges φ i x

Uses 5 · Used by 1

Statement usesArcs of a variable diamond · Row vertices of a diamond · CNF formula · CNF clause

Proof usesTops of the diamonds

Used byA satisfying choice gives a Hamiltonian path

TheoremPositive detour arcs of a diamond#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses, let \(i\), \(x\), \(j\) be natural numbers with \(j < m\), and write \(r_i(l)\) for row vertex \(l\) of diamond \(i\). If the variable \(x\) occurs positively in clause \(j\) of \(\varphi\) (counting clauses from \(0\)), then the arcs of diamond \(i\) for variable \(x\) include both the arc from \(r_i(3j+1)\) to clause vertex \(j\) and the arc from clause vertex \(j\) to \(r_i(3j+2)\).

theorem mem_diamondEdges_pos {φ : CNF} {i x j : ℕ} (hj : j < φ.length)
    (h : (x, true) ∈ φ.getD j []) :
    (hpR φ.length i (3 * j + 1), j) ∈ diamondEdges φ i x ∧
      (j, hpR φ.length i (3 * j + 2)) ∈ diamondEdges φ i x

Uses 5 · Used by 1

Statement usesArcs of a variable diamond · Row vertices of a diamond · CNF formula · CNF clause

Proof usesTops of the diamonds

Used byA satisfying choice gives a Hamiltonian path

TheoremThe detour arcs of a negative occurrence#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses, let \(i\), \(x\) and \(j\) be natural numbers with \(j < m\), and write \(r_l = m + i(3m + 2) + 1 + l\) for the row vertices of diamond \(i\). If the negative literal \(\neg x\) occurs in clause \(j\) of \(\varphi\), then \((r_{3j+2}, j)\) and \((j, r_{3j+1})\) are arcs of diamond \(i\) for the variable \(x\) in the construction for \(\varphi\).

theorem mem_diamondEdges_neg {φ : CNF} {i x j : ℕ} (hj : j < φ.length)
    (h : (x, false) ∈ φ.getD j []) :
    (hpR φ.length i (3 * j + 2), j) ∈ diamondEdges φ i x ∧
      (j, hpR φ.length i (3 * j + 1)) ∈ diamondEdges φ i x

Uses 5 · Used by 1

Statement usesArcs of a variable diamond · Row vertices of a diamond · CNF formula · CNF clause

Proof usesTops of the diamonds

Used byA satisfying choice gives a Hamiltonian path

TheoremA satisfying choice gives a Hamiltonian path#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses, let \(v_0, \dots, v_{k-1}\) be its distinct variables in the order used by the construction, let \(\sigma\) assign a truth value to every variable, and write \(t_a = m + a(3m + 2)\) for the top of diamond \(a\). Let \(c : \mathbb{N} \to \mathbb{N}\) be such that for every \(j < m\) we have \(c(j) < k\) and clause \(j\) of \(\varphi\) contains the literal over \(v_{c(j)}\) that \(\sigma\) makes true (positive if \(\sigma(v_{c(j)})\) is true, negative otherwise). Then the forward path through the first \(k\) diamonds for \(c\), with diamond \(i\) traversed in direction \(\sigma(v_i)\), is a Hamiltonian path from \(t_0\) to \(t_k\) in the digraph on the vertices \(0, \dots, t_k\) whose arcs are the arcs of the construction for \(\varphi\).

theorem isHamPath_hfPath {φ : CNF} {σ : ℕ → Bool} {c : ℕ → ℕ}
    (hc : ∀ j < φ.length, c j < (hamVars φ).length ∧
      ((hamVars φ).getD (c j) 0, σ ((hamVars φ).getD (c j) 0)) ∈ φ.getD j []) :
    IsHamPath (hpT φ.length (hamVars φ).length + 1) (hamEdges φ) (hpT φ.length 0)
      (hpT φ.length (hamVars φ).length)
      (hfPath φ.length (hamVars φ).length c fun i => σ ((hamVars φ).getD i 0))

Uses 23 · Used by 1

Statement usesHamiltonian paths · Arcs of the HAMPATH construction · Distinct variables of a formula · The forward path through the diamonds · Tops of the diamonds · CNF formula · CNF clause

Proof usesArcs of a variable diamond · The forward path ends at the last top · The forward path starts at the first top · The visit of a diamond · The forward path visits every vertex once · Row vertices of a diamond · Row vertices lie below the next top · Tops are monotone in the diamond index · Chain condition for a diamond traversal · Chain condition for the forward path · The frame arcs of a diamond · The detour arcs of a negative occurrence · Positive detour arcs of a diamond · Row arcs of a diamond · Diamond arcs are arcs of the construction · Arcs of the PATH digraph

Used bySatisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction)

TheoremSatisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction)#✓fully proved

Let \(\varphi\) be a satisfiable CNF formula with \(m\) clauses and \(k\) distinct variables, and let \(T_i = m + i(3m+2)\) be the top of diamond \(i\). Then the digraph on the vertices \(0, \dots, T_k\) whose arcs are the arcs of the HAMPATH construction for \(\varphi\) has a Hamiltonian path from \(T_0\) to \(T_k\).

theorem exists_isHamPath_of_cnfSat {φ : CNF} (h : CNFSat φ) :
    ∃ p, IsHamPath (hpT φ.length (hamVars φ).length + 1) (hamEdges φ)
      (hpT φ.length 0) (hpT φ.length (hamVars φ).length) p

Uses 11 · 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 usesThe forward path through the diamonds · A satisfying choice gives a Hamiltonian path · Variables of a formula occur in its occurrence list · Occurrence list of a CNF formula

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

TheoremOut-neighbours of a top#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses. In Sipser's HAMPATH graph for \(\varphi\), every arc out of the top \(t_i\) of diamond \(i\) ends at one of the two ends \(r_{i,0}\) and \(r_{i,3m}\) of the row of diamond \(i\).

theorem hpT_arc {φ : CNF} {i v : ℕ} (h : (hpT φ.length i, v) ∈ hamEdges φ) :
    v = hpR φ.length i 0 ∨ v = hpR φ.length i (3 * φ.length)

Uses 8 · Used by 1

Statement usesArcs of the HAMPATH construction · Row vertices of a diamond · Tops of the diamonds · CNF formula · CNF clause

Proof usesClassification of the arcs of Sipser's graph · Distinct variables of a formula · Tops of distinct diamonds are at least \(3m + 2\) apart

Used byEvery top but the last is followed by an end of its row

TheoremArcs from a row into a clause vertex#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses \(C_0, \dots, C_{m-1}\), and let \(x_i\) be the \(i\)-th of its distinct variables (variable \(0\) if \(\varphi\) has at most \(i\) distinct variables). In Sipser's HAMPATH graph for \(\varphi\), clause \(j\) is vertex \(j\), and \(r_{i,l}\) denotes vertex \(l\) of the row of diamond \(i\). If \(l \le 3m\), \(j < m\) and \((r_{i,l}, j)\) is an arc of the graph, then either \(l = 3j + 1\) and the literal \(x_i\) occurs in \(C_j\), or \(l = 3j + 2\) and the literal \(\neg x_i\) occurs in \(C_j\).

theorem hpR_arc_clause {φ : CNF} {i l j : ℕ} (hl : l ≤ 3 * φ.length) (hj : j < φ.length)
    (h : (hpR φ.length i l, j) ∈ hamEdges φ) :
    (l = 3 * j + 1 ∧ ((hamVars φ).getD i 0, true) ∈ φ.getD j []) ∨
      (l = 3 * j + 2 ∧ ((hamVars φ).getD i 0, false) ∈ φ.getD j [])

Uses 8 · Used by 1

Statement usesArcs of the HAMPATH construction · Distinct variables of a formula · Row vertices of a diamond · CNF formula · CNF clause

Proof usesTops of the diamonds · Tops of distinct diamonds are at least \(3m + 2\) apart · Arcs of the Hamiltonian path construction

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

DefinitionRow vertices counted from either end#✓fully proved

For \(m\) clauses, let \(r_{i,l} = m + i(3m + 2) + 1 + l\) be vertex \(l\) of the row of diamond \(i\). For a Boolean \(b\) and a natural number \(l\), this is \(r_{i,l}\) if \(b\) is true and \(r_{i,3m - l}\) if \(b\) is false, where \(3m - l\) is truncated subtraction (\(0\) when \(l > 3m\)). For \(l \le 3m\) it is vertex \(l\) of the row counted from the left end (\(b\) true) or from the right end (\(b\) false).

def hpRo (m i : ℕ) (b : Bool) (l : ℕ) : ℕ := hpR m i (if b then l else 3 * m - l)

Uses 1 · Used by 6

Statement usesRow vertices of a diamond

Used byIn-neighbours of a row vertex outside the clause vertices · Out-neighbours of a row vertex outside the clause vertices · Backward direction of SAT ≤ HAMPATH for paths with normal detours · Every top but the last is followed by an end of its row · Entering a row and leaving it at once is impossible · A row entered at one end is run to the other end

TheoremOut-neighbours of a row vertex outside the clause vertices#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses. 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 \(t_{i+1}\) is its bottom), and \(\rho_b(i, l)\) denotes vertex \(l\) of the row of diamond \(i\) counted from the left end if \(b\) is true and from the right end if \(b\) is false. Let \(l \le 3m\) and \(v \ge m\). If \((\rho_b(i, l), v)\) is an arc of the graph, then \(l < 3m\) and \(v = \rho_b(i, l + 1)\), or \(l > 0\) and \(v = \rho_b(i, l - 1)\), or \(l \in \{0, 3m\}\) and \(v = t_{i+1}\).

theorem hpRo_arc {φ : CNF} {i l v : ℕ} {b : Bool} (hl : l ≤ 3 * φ.length)
    (hv : φ.length ≤ v) (h : (hpRo φ.length i b l, v) ∈ hamEdges φ) :
    (l < 3 * φ.length ∧ v = hpRo φ.length i b (l + 1)) ∨
      (0 < l ∧ v = hpRo φ.length i b (l - 1)) ∨
      ((l = 0 ∨ l = 3 * φ.length) ∧ v = hpT φ.length (i + 1))

Uses 7 · Used by 1

Statement usesArcs of the HAMPATH construction · Row vertices counted from either end · Tops of the diamonds · CNF formula · CNF clause

Proof usesOut-neighbours of a row vertex in Sipser's graph · Row vertices of a diamond

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

TheoremIn-neighbours of a row vertex outside the clause vertices#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses. 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 \(\rho_b(i, l)\) denotes vertex \(l\) of the row of diamond \(i\) counted from the left end if \(b\) is true and from the right end if \(b\) is false. Let \(l \le 3m\) and \(u \ge m\). If \((u, \rho_b(i, l))\) is an arc of the graph, then \(l > 0\) and \(u = \rho_b(i, l - 1)\), or \(l < 3m\) and \(u = \rho_b(i, l + 1)\), or \(l \in \{0, 3m\}\) and \(u = t_i\).

theorem arc_hpRo {φ : CNF} {i l u : ℕ} {b : Bool} (hl : l ≤ 3 * φ.length)
    (hu : φ.length ≤ u) (h : (u, hpRo φ.length i b l) ∈ hamEdges φ) :
    (0 < l ∧ u = hpRo φ.length i b (l - 1)) ∨
      (l < 3 * φ.length ∧ u = hpRo φ.length i b (l + 1)) ∨
      ((l = 0 ∨ l = 3 * φ.length) ∧ u = hpT φ.length i)

Uses 7 · Used by 1

Statement usesArcs of the HAMPATH construction · Row vertices counted from either end · Tops of the diamonds · CNF formula · CNF clause

Proof usesIn-neighbours of a row vertex in Sipser's graph · Row vertices of a diamond

Used byEntering a row and leaving it at once is impossible

DefinitionDeleting the clause vertices from a path#✓fully proved

For a CNF formula \(\varphi\) with \(m\) clauses (the clause vertices of Sipser's HAMPATH graph are \(0, \dots, m - 1\)) and a list \(p\) of natural numbers, the list obtained from \(p\) by deleting every entry \(v < m\), keeping the other entries in their order.

def dropClauses (φ : CNF) (p : List ℕ) : List ℕ := p.filter fun v => decide (φ.length ≤ v)

Uses 2 · Used by 7

Statement usesCNF formula · CNF clause

Used byConsecutive vertices of the contracted path are joined by arcs · Contracting a clause detour · Backward direction of SAT ≤ HAMPATH for paths with normal detours · Every vertex of the contracted path except its end has a successor · Every top but the last is followed by an end of its row · Entering a row and leaving it at once is impossible · A row entered at one end is run to the other end

TheoremContracting a clause detour#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses, let \(p\) be a list of natural numbers, and let \(q\) be the list obtained from \(p\) by deleting every entry less than \(m\). If \(a, j, c\) occur consecutively in \(p\) with \(j < m\), \(a \ge m\) and \(c \ge m\), then \(a\) is immediately followed by \(c\) in \(q\).

theorem infix_dropClauses {a j c : ℕ} (hp : [a, j, c] <:+: p) (hj : j < φ.length)
    (ha : φ.length ≤ a) (hc : φ.length ≤ c) : [a, c] <:+: dropClauses φ p

Uses 3 · Used by 1

Statement usesDeleting the clause vertices from a path · CNF formula · CNF clause

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

TheoremConsecutive vertices of the contracted path are joined by arcs#✓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. If \(v\) comes right after \(u\) in \(p'\), then \((u, v)\) is an arc of the graph, \(u \ge m\) and \(v \ge m\).

theorem arc_of_infix_dropClauses {u v : ℕ} (hd : DetoursNormal φ p)
    (huv : [u, v] <:+: dropClauses φ p) :
    (u, v) ∈ hamEdges φ ∧ φ.length ≤ u ∧ φ.length ≤ v

Uses 12 · Used by 3

Statement usesNormal clause detours · Hamiltonian 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 usesRow vertices of a diamond · Arcs of the Hamiltonian path construction · A Hamiltonian path visits every vertex · Arcs of the PATH digraph

Used byEvery top but the last is followed by an end of its row · Entering a row and leaving it at once is impossible · A row entered at one end is run to the other end

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.