Hamiltonian paths to Witness encoding of a nonempty list

DefinitionHamiltonian paths#✓fully proved

Let \(E\) be a list of pairs of natural numbers, viewed as the digraph on \(0, \dots, n - 1\) whose arcs are the pairs in \(E\) with both ends below \(n\). A list \(p\) is a Hamiltonian path from \(s\) to \(t\) when it lists each of the vertices \(0, \dots, n - 1\) exactly once, starts at \(s\), ends at \(t\), and each two consecutive entries of \(p\) form an arc.

def IsHamPath (n : ℕ) (es : List (ℕ × ℕ)) (s t : ℕ) (p : List ℕ) : Prop :=
  p.Nodup ∧ p.length = n ∧ (∀ v ∈ p, v < n) ∧ p.head? = some s ∧ p.getLast? = some t ∧
    p.IsChain (Path.arc n es)

Uses 1 · Used by 23

Statement usesArcs of the PATH digraph

Used byThe HAMPATH problem · What the HAMPATH verifier accepts · The Hamiltonian path check is correct · Hamiltonian paths of Sipser's graph have normal detours · Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs · HAMPATH is verified with quadratic-size witnesses · A clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · A Hamiltonian path visits every vertex · The machine's walk is the check · Consecutive vertices of the contracted path are joined by arcs · Satisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction) · A satisfying choice gives a Hamiltonian path · Backward direction of SAT ≤ HAMPATH for paths with normal detours · Every vertex of the contracted path except its end has a successor · The construction has a Hamiltonian path iff the formula is satisfiable · Every top but the last is followed by an end of its row · HAMPATH on an encoded instance · HAMPATH rejects the fixed no-instance · Entering a row and leaving it at once is impossible · A row entered at one end is run to the other end · SAT ≤ HAMPATH preserves membership

DefinitionThe HAMPATH problem#✓fully proved

The decision problem that accepts a bit string \(x\) exactly when, for some \(s\), \(t\), \(n\) and list of pairs \(E\), \(x\) is the PATH encoding of \(s\), \(t\) and the digraph on \(0, \dots, n - 1\) with edge list \(E\), and this digraph has a Hamiltonian path from \(s\) to \(t\).

noncomputable def hamPathDec : MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  decide (∃ s t n es, Path.encodeP s t n es = x ∧ ∃ p, IsHamPath n es s t p)

Uses 3 · Used by 7

Statement usesHamiltonian paths · Encoding of a PATH instance · Decision problems

Used byHAMPATH is verified with quadratic-size witnesses · HAMPATH on an encoded instance · HAMPATH rejects the fixed no-instance · SAT ≤ HAMPATH preserves membership · HAMPATH is in NP · HAMPATH is NP-complete · HAMPATH is NP-hard

DefinitionDistinct variables of a formula#✓fully proved

The list of the distinct variables of a CNF formula \(\varphi\), in order of occurrence in \(\varphi\), with each variable kept at its last occurrence.

def hamVars (φ : CNF) : List ℕ := (varsOf φ).dedup

Uses 2 · Used by 33

Statement usesOccurrence list of a CNF formula · CNF formula

Used byNormal clause detours · Arcs of the HAMPATH construction · Sipser's HAMPATH instance of a CNF formula · Hamiltonian paths of Sipser's graph have normal detours · Classification of the arcs of Sipser's graph · Out-neighbours of a clause vertex in Sipser's graph · Out-neighbours of a row vertex in Sipser's graph · Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs · In-neighbours of a clause vertex in Sipser's graph · In-neighbours of a row vertex in Sipser's graph · A clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · Arcs of the Hamiltonian path construction · The HAMPATH instance as unary blocks and arc bits · The emitter state before the diamonds · Phase A of the HAMPATH emitter · The diamonds · Correctness and running time of the HAMPATH emitter · Consecutive vertices of the contracted path are joined by arcs · Satisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction) · Arcs from a row into a clause vertex · Out-neighbours of a top · A satisfying choice gives a Hamiltonian path · Diamond arcs are arcs of the construction · Backward direction of SAT ≤ HAMPATH for paths with normal detours · Every vertex of the contracted path except its end has a successor · The construction has a Hamiltonian path iff the formula is satisfiable · Every top but the last is followed by an end of its row · Positions in the list of distinct variables · Entering a row and leaving it at once is impossible · A row entered at one end is run to the other end · SAT ≤ HAMPATH preserves membership

DefinitionTops of the diamonds#✓fully proved

In the HAMPATH construction with \(m\) clauses, the top of diamond \(i\) is the vertex \(m + i(3m + 2)\); it is also the bottom of diamond \(i - 1\).

def hpT (m i : ℕ) : ℕ := m + i * (3 * m + 2)

Used by 56

Used byArcs of a variable diamond · Row vertices of a diamond · Row vertices lie below the next top · Tops are monotone in the diamond index · Sipser's HAMPATH instance of a CNF formula · Hamiltonian paths of Sipser's graph have normal detours · The frame of a diamond · Classification of the arcs of Sipser's graph · Out-neighbours of a clause vertex in Sipser's graph · Out-neighbours of a row vertex in Sipser's graph · Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs · In-neighbours of a clause vertex in Sipser's graph · In-neighbours of a row vertex in Sipser's graph · A clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · Tops of distinct diamonds are at least \(3m + 2\) apart · Arcs of the Hamiltonian path construction · The HAMPATH instance as unary blocks and arc bits · Consecutive row vertices · The next diamond top follows the row · Front of a diamond · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · The detours of a diamond · One diamond · The diamonds · The row of a diamond in the HAMPATH emitter · The first \(t\) diamonds occupy consecutive vertices · The visit of a diamond · A diamond visit is a block of consecutive vertices plus its clauses · The forward path through the diamonds · The forward path visits every vertex once · Correctness and running time of the HAMPATH emitter · In-neighbours of a row vertex outside the clause vertices · Consecutive vertices of the contracted path are joined by arcs · 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 · Arcs from a row into a clause vertex · Out-neighbours of a row vertex outside the clause vertices · Out-neighbours of a top · Chain condition for a diamond traversal · Chain condition for the forward path · A satisfying choice gives a Hamiltonian 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 · Backward direction of SAT ≤ HAMPATH for paths with normal detours · Every vertex of the contracted path except its end has a successor · The construction has a Hamiltonian path iff the formula is satisfiable · 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 · SAT ≤ HAMPATH preserves membership

DefinitionRow vertices of a diamond#✓fully proved

In the HAMPATH construction with \(m\) clauses, write \(T(i)\) for the top of diamond \(i\). Row vertex \(l\) of diamond \(i\) is the number \(T(i) + 1 + l\); the row of diamond \(i\) consists of the vertices with \(l \le 3m\).

def hpR (m i l : ℕ) : ℕ := hpT m i + 1 + l

Uses 1 · Used by 48

Statement usesTops of the diamonds

Used byNormal clause detours · Arcs of a variable diamond · Row vertices lie below the next top · Hamiltonian paths of Sipser's graph have normal detours · The frame of a diamond · Classification of the arcs of Sipser's graph · Out-neighbours of a clause vertex in Sipser's graph · Out-neighbours of a row vertex in Sipser's graph · In-neighbours of a clause vertex in Sipser's graph · In-neighbours of a row vertex in Sipser's graph · A clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · Arcs of the Hamiltonian path construction · Clause detours in a diamond · Consecutive row vertices · The next diamond top follows the row · The row arcs of a diamond · One clause of the detour walk · Front of a diamond · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · The detours of a diamond · One diamond · The row of a diamond in the HAMPATH emitter · A row starts at its left end · A diamond visit is a block of consecutive vertices plus its clauses · The row of a diamond with its clauses inserted · The vertices of a diamond row · Chain condition for a diamond row · Correctness and running time of the HAMPATH emitter · In-neighbours of a row vertex outside the clause vertices · Consecutive vertices of the contracted path are joined by arcs · A row ends at its right end · Arcs from a row into a clause vertex · Row vertices counted from either end · Out-neighbours of a row vertex outside the clause vertices · Out-neighbours of a top · Chain condition for a diamond traversal · A satisfying choice gives a Hamiltonian 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 · 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

DefinitionArcs of a variable diamond#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses, and write \(T(i)\) for the top of diamond \(i\) and \(R(i, l)\) for its row vertex \(l\). The arcs of diamond \(i\) for variable \(x\) are \(T(i) \to R(i, 0)\), \(T(i) \to R(i, 3m)\), \(R(i, 0) \to T(i + 1)\) and \(R(i, 3m) \to T(i + 1)\); for every \(l < 3m\), both \(R(i, l) \to R(i, l + 1)\) and \(R(i, l + 1) \to R(i, l)\); and for every clause \(j < m\), the arcs \(R(i, 3j + 1) \to j\) and \(j \to R(i, 3j + 2)\) if \(x\) occurs positively in clause \(j\), and the arcs \(R(i, 3j + 2) \to j\) and \(j \to R(i, 3j + 1)\) if \(x\) occurs negatively in clause \(j\). Here \(j\) is the vertex of clause \(j\).

def diamondEdges (φ : CNF) (i x : ℕ) : List (ℕ × ℕ) :=
  let m := φ.length
  [(hpT m i, hpR m i 0), (hpT m i, hpR m i (3 * m)), (hpR m i 0, hpT m (i + 1)),
    (hpR m i (3 * m), hpT m (i + 1))] ++
  (List.range (3 * m)).flatMap (fun l => [(hpR m i l, hpR m i (l + 1)),
    (hpR m i (l + 1), hpR m i l)]) ++
  (List.range m).flatMap fun j =>
    (if (x, true) ∈ φ.getD j [] then [(hpR m i (3 * j + 1), j), (j, hpR m i (3 * j + 2))]
      else []) ++
    (if (x, false) ∈ φ.getD j [] then [(hpR m i (3 * j + 2), j), (j, hpR m i (3 * j + 1))]
      else [])

Uses 4 · Used by 10

Statement usesRow vertices of a diamond · Tops of the diamonds · CNF formula · CNF clause

Used byArcs of the HAMPATH construction · One diamond · The diamonds · Correctness and running time of the HAMPATH emitter · A satisfying choice gives a Hamiltonian 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

DefinitionArcs of the HAMPATH construction#✓fully proved

Let \(\varphi\) be a CNF formula and let \(x_0, \dots, x_{k-1}\) be its distinct variables, in the order of the distinct-variable list of \(\varphi\). The arcs of the construction for \(\varphi\) are the arcs of diamond \(i\) for variable \(x_i\), for \(i = 0, \dots, k - 1\), concatenated in this order.

def hamEdges (φ : CNF) : List (ℕ × ℕ) :=
  (List.range (hamVars φ).length).flatMap fun i => diamondEdges φ i ((hamVars φ).getD i 0)

Uses 3 · Used by 30

Statement usesArcs of a variable diamond · Distinct variables of a formula · CNF formula

Used bySipser's HAMPATH instance of a CNF formula · Hamiltonian paths of Sipser's graph have normal detours · Classification of the arcs of Sipser's graph · Out-neighbours of a clause vertex in Sipser's graph · Out-neighbours of a row vertex in Sipser's graph · Consecutive vertices of a Hamiltonian path of Sipser's graph form arcs · In-neighbours of a clause vertex in Sipser's graph · In-neighbours of a row vertex in Sipser's graph · A clause detour returns to its own pair (Sipser's separator argument) · A Hamiltonian path of Sipser's graph does not cross a diamond through one row end · A separator is next to each of its row neighbours on a Hamiltonian path · Arcs of the Hamiltonian path construction · The HAMPATH instance as unary blocks and arc bits · The diamonds · Correctness and running time of the HAMPATH emitter · In-neighbours of a row vertex outside the clause vertices · Consecutive vertices of the contracted path are joined by arcs · Satisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction) · Arcs from a row into a clause vertex · Out-neighbours of a row vertex outside the clause vertices · Out-neighbours of a top · A satisfying choice gives a Hamiltonian path · Diamond arcs are arcs of the construction · Backward direction of SAT ≤ HAMPATH for paths with normal detours · Every vertex of the contracted path except its end has a successor · The construction has a Hamiltonian path iff the formula is satisfiable · 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 · SAT ≤ HAMPATH preserves membership

DefinitionSipser's HAMPATH instance of a CNF formula#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses, numbered \(0, \dots, m - 1\), and let \(x_0, \dots, x_{k-1}\) be its distinct variables, in the order of their last occurrences in \(\varphi\) (clauses read in order, and the literals of each clause in order). Put \(T_i = m + i(3m + 2)\) and \(R_{i,l} = T_i + 1 + l\). The result is the encoded PATH instance with vertices \(0, \dots, T_k\), source \(T_0\), target \(T_k\), and, for each \(i < k\), the following arcs: the frame arcs \(T_i \to R_{i,0}\), \(T_i \to R_{i,3m}\), \(R_{i,0} \to T_{i+1}\) and \(R_{i,3m} \to T_{i+1}\); the row arcs \(R_{i,l} \to R_{i,l+1}\) and \(R_{i,l+1} \to R_{i,l}\) for every \(l < 3m\); and, for every clause \(j < m\), the arcs \(R_{i,3j+1} \to j\) and \(j \to R_{i,3j+2}\) if the literal \(x_i\) occurs in clause \(j\), and the arcs \(R_{i,3j+2} \to j\) and \(j \to R_{i,3j+1}\) if the literal \(\neg x_i\) occurs in clause \(j\).

def toHam (φ : CNF) : List Bool :=
  Path.encodeP (hpT φ.length 0) (hpT φ.length (hamVars φ).length)
    (hpT φ.length (hamVars φ).length + 1) (hamEdges φ)

Uses 6 · Used by 6

Statement usesArcs of the HAMPATH construction · Distinct variables of a formula · Tops of the diamonds · Encoding of a PATH instance · CNF formula · CNF clause

Used byThe SAT-to-HAMPATH reduction map · The HAMPATH instance as unary blocks and arc bits · Correctness and running time of the HAMPATH emitter · SAT ≤ HAMPATH preserves membership · The HAMPATH emitter · SAT ≤ HAMPATH is polynomial-time

DefinitionA fixed HAMPATH no-instance#✓fully proved

The encoded PATH instance on the two vertices \(0\) and \(1\), with no arcs, whose source and target are both \(0\).

It is a no-instance of HAMPATH: a Hamiltonian path would visit both vertices and start and end at \(0\), so it would visit \(0\) twice.

def noHam : List Bool := Path.encodeP 0 0 2 []

Uses 1 · Used by 5

Statement usesEncoding of a PATH instance

Used byThe SAT-to-HAMPATH reduction map · HAMPATH rejects the fixed no-instance · SAT ≤ HAMPATH preserves membership · The HAMPATH emitter · SAT ≤ HAMPATH is polynomial-time

DefinitionThe SAT-to-HAMPATH reduction map#✓fully proved

A bit string \(x\) that decodes to a CNF formula \(\varphi\) is sent to Sipser's HAMPATH instance of \(\varphi\), and a bit string that does not decode to a CNF formula is sent to the fixed HAMPATH no-instance (two vertices, no arcs, source and target \(0\)).

def reduceHam (x : List Bool) : List Bool :=
  match decodeCNF x with
  | some φ => toHam φ
  | none => noHam

Uses 4 · Used by 3

Statement usesA fixed HAMPATH no-instance · Sipser's HAMPATH instance of a CNF formula · Decoding a complete length-prefixed CNF formula · CNF formula

Used bySAT ≤ HAMPATH preserves membership · HAMPATH is NP-hard · SAT ≤ HAMPATH is polynomial-time

DefinitionNormal clause detours#✓fully proved

Let \(\varphi\) be a CNF formula with \(m\) clauses and \(k\) distinct variables, and write \(R(i, l)\) for row vertex \(l\) of diamond \(i\) in the HAMPATH construction for \(\varphi\). A list of vertices \(p\) has normal detours when for every clause \(j < m\) there is a diamond \(i < k\) such that \(p\) contains \(R(i, 3j + 1), j, R(i, 3j + 2)\) or \(R(i, 3j + 2), j, R(i, 3j + 1)\) as consecutive entries.

def DetoursNormal (φ : CNF) (p : List ℕ) : Prop :=
  ∀ j < φ.length, ∃ i < (hamVars φ).length,
    [hpR φ.length i (3 * j + 1), j, hpR φ.length i (3 * j + 2)] <:+: p ∨
      [hpR φ.length i (3 * j + 2), j, hpR φ.length i (3 * j + 1)] <:+: p

Uses 4 · Used by 6

Statement usesDistinct variables of a formula · Row vertices of a diamond · CNF formula · CNF clause

Used byHamiltonian paths of Sipser's graph have normal detours · Consecutive vertices of the contracted path are joined by arcs · 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

TheoremTops are monotone in the diamond index#✓fully proved

In the HAMPATH construction with \(m\) clauses, if \(i \le i'\) then the top of diamond \(i\) is at most the top of diamond \(i'\).

theorem hpT_mono {m i i' : ℕ} (h : i ≤ i') : hpT m i ≤ hpT m i'

Uses 1 · Used by 6

Statement usesTops of the diamonds

Used byThe diamonds · Correctness and running time of the HAMPATH emitter · A satisfying choice gives a Hamiltonian path · 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

TheoremRow vertices lie below the next top#✓fully proved

In the HAMPATH construction with \(m\) clauses, for every diamond \(i\) and every \(l \le 3m\), row vertex \(l\) of diamond \(i\) is a smaller number than the top of diamond \(i + 1\).

theorem hpR_lt_hpT_succ {m i l : ℕ} (hl : l ≤ 3 * m) : hpR m i l < hpT m (i + 1)

Uses 2 · Used by 3

Statement usesRow vertices of a diamond · Tops of the diamonds

Used byA satisfying choice gives a Hamiltonian path · Entering a row and leaving it at once is impossible · A row entered at one end is run to the other end

TheoremBits of an edge list, first edge first#✓fully proved

For natural numbers \(u, v\) and a list \(E\) of pairs of natural numbers, the bit encoding of the edge list whose first edge is \((u, v)\) and whose remaining edges are \(E\) is: \(u\) copies of true, then false, then \(v\) copies of true, then false, then the bit encoding of \(E\).

theorem edgeBits_cons (u v : ℕ) (es : List (ℕ × ℕ)) : Karp.edgeBits ((u, v) :: es) =
    List.replicate u true ++ false :: (List.replicate v true ++ false :: Karp.edgeBits es)

Uses 1 · Used by 2

Statement usesBit encoding of an edge list

Used byLength bound for the bit encoding of an edge list · The edge scan of the Hamiltonian path verifier

TheoremEdge bits of the empty edge list#✓fully proved

The edge-list bit encoding of the empty list of edges is the empty bit string.

@[simp] theorem edgeBits_nil : Karp.edgeBits [] = []

Uses 1

Statement usesBit encoding of an edge list

TheoremBits of concatenated edge lists#✓fully proved

For all lists \(E\) and \(E'\) of pairs of natural numbers, the bit encoding of the concatenation of \(E\) and \(E'\) is the bit encoding of \(E\) followed by the bit encoding of \(E'\).

theorem edgeBits_append (es es' : List (ℕ × ℕ)) :
    Karp.edgeBits (es ++ es') = Karp.edgeBits es ++ Karp.edgeBits es'

Uses 1 · Used by 6

Statement usesBit encoding of an edge list

Used byOne clause of the detour walk · The row loop of a diamond in the HAMPATH emitter · The detour walk of a diamond in the HAMPATH emitter · One diamond · The diamonds · The edge scan of the Hamiltonian path verifier

DefinitionWitness encoding#✓fully proved

The witness encoding of a list \(p\) of natural numbers (the vertices of a candidate path) is the bit string obtained by writing each entry \(v\) of \(p\), in order, as \(v\) copies of true followed by one false, and concatenating the results.

def encW (p : List ℕ) : List Bool := p.flatMap fun v => List.replicate v true ++ [false]

Used by 19

Used byWitness encoding of a nonempty list · Witness encoding of the empty list · Decoding inverts the witness encoding · The witness codec · The witness encoding respects concatenation · The witness decoder succeeds only on encodings · The verifier on an encoded instance and witness · What the HAMPATH verifier accepts · Witness length · Witness length bound · A witness is at least as long as its vertex list · HAMPATH is verified with quadratic-size witnesses · Running the head-or-edge check · Stack layout between vertex steps · 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

DefinitionWitness decoder#✓fully proved

The witness decoder reads a list \(w\) of bits as a list of natural numbers. On the empty list it returns the empty list. Otherwise it reads a unary number \(v\) from the front of \(w\), a run of \(v\) copies of true ended by false, and if decoding the remaining bits gives a list \(p\), it returns \(v\) followed by \(p\). It fails if no unary number can be read from a nonempty list, or if decoding the remaining bits fails.

def decodeW (w : List Bool) : Option (List ℕ) :=
  if w = [] then some [] else
    match h : readUnaryLength w with
    | none => none
    | some (v, r) =>
        have : r.length < w.length := Karp.length_lt_of_readUnaryLength h
        (decodeW r).map (v :: ·)
termination_by w.length

Uses 2 · Used by 13

Statement usesReading a unary number shortens the input · Reading a unary length prefix

Used byDecoding inverts the witness encoding · The witness codec · Decoding the empty witness · Witness decoding fails on a cut-off first number · Decoding peels off the first number · The witness decoder succeeds only on encodings · The HAMPATH verifier · The verifier on an encoded instance and witness · What the HAMPATH verifier accepts · Instances that do not decode are rejected · Witnesses that do not decode are rejected · The witness check of the Hamiltonian-path verifier · Correctness and running time of the Hamiltonian path verifier

TheoremWitness encoding of the empty list#✓fully proved

The witness encoding of the empty list of vertices is the empty bit string.

@[simp] theorem encW_nil : encW [] = []

Uses 1

Statement usesWitness encoding

TheoremWitness encoding of a nonempty list#✓fully proved

For a natural number \(v\) and a list \(p\) of natural numbers, the witness encoding of the list with first entry \(v\) followed by \(p\) is the bit string made of \(v\) copies of true, then one false, then the witness encoding of \(p\).

theorem encW_cons (v : ℕ) (p : List ℕ) :
    encW (v :: p) = List.replicate v true ++ false :: encW p

Uses 1 · Used by 7

Statement usesWitness encoding

Used byDecoding inverts the witness encoding · The witness decoder succeeds only on encodings · Witness length · Witness length bound · Running the vertex loop · The repeat scan of the Hamiltonian path verifier · 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.