The row-by-row check is the pairwise check to Labels of the CLIQUE verifier

TheoremThe row-by-row check is the pairwise check#✓fully proved

For every mode \(m\) and all lists of bits \(s\) and \(b\), the row-by-row check of \(s\) against \(b\) holds if and only if \(b\) has exactly one bit per pair \(i < j < |s|\) and, listing these pairs in encoding order (rows \(i\) ascending, within a row \(j\) descending), the \(t\)-th pair \((i, j)\) and the \(t\)-th bit \(b_t\) satisfy the pair condition \(\mathrm{ok}_m(b_t, s_i, s_j)\) for every \(t\).

theorem rowsOk_eq (m : Mode) : ∀ (s bs : List Bool), rowsOk m s bs =
    (bs.length == (pairVals s).length &&
      ((pairVals s).zip bs).all fun q => m.ok q.2 q.1.1 q.1.2)

Uses 9 · Used by 1

Statement usesModes of the clique verifier · Pair condition of the clique verifier · Chosen-flag pairs · The row-by-row check of the clique verifier

Proof usesVertices that settle their pairs alone · The pair condition splits by vertex · The pair condition left to the later vertex · Chosen-flag pairs of a list with a new head · Vertex pairs in encoding order

Used byThe verifier as a row-by-row check

TheoremThe verifier as a row-by-row check#✓fully proved

Let \(m\) be a mode and \(x\), \(w\) bit lists. Suppose that \(x\) decodes to \((k, n, \mathit{bits})\), that \(w\) has at least \(n\) bits, and that exactly \(k\) of the first \(n\) bits of \(w\) are set. Then the verifier for mode \(m\) on input \(x\) and witness \(w\) returns the same value as the row-by-row check for mode \(m\) of the first \(n\) bits of \(w\) against the pair bits \(\mathit{bits}\).

theorem kgCheck_eq_rowsOk {m : Mode} {x w : List Bool} {k n : ℕ} {bits : List Bool}
    (hx : decodeKG x = some (k, n, bits)) (hn : n ≤ w.length) (hk : (w.take n).count true = k) :
    kgCheck m x w = rowsOk m (w.take n) bits

Uses 9 · Used by 1

Statement usesModes of the clique verifier · The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · The row-by-row check of the clique verifier · Decoding a graph instance

Proof usesPair condition of the clique verifier · Chosen-flag pairs · The row-by-row check is the pairwise check · Membership in the vertex pairs · Vertex pairs in encoding order

Used byThe verifier machine for clique, independent set and vertex cover

TheoremLookup in a list of pairs with distinct keys#✓fully proved

Let \(l\) be a list of pairs whose keys lie in a type with a lawful Boolean equality and are pairwise distinct. If \((a, b)\) occurs in \(l\), then looking up the key \(a\) in \(l\) returns \(b\).

theorem lookup_of_mem {α β : Type} [BEq α] [LawfulBEq α] :
    ∀ {l : List (α × β)} {a : α} {b : β}, (l.map Prod.fst).Nodup → (a, b) ∈ l →
      l.lookup a = some b

Used by 1

Used byChecking each listed vertex pair against its bit

TheoremChecking each listed vertex pair against its bit#✓fully proved

Let \(n\) be a natural number and \(b\) a list of bits with one bit per vertex pair, that is, with as many entries as the list of pairs \((i, j)\) with \(i < j < n\). Then for every Boolean predicate \(P\) on a pair of natural numbers and a bit, \(P\) holds on every entry of the pair list zipped with \(b\) (the \(t\)-th pair together with the \(t\)-th bit of \(b\)) if and only if, for all natural numbers \(i < j < n\), \(P\) holds on the pair \((i, j)\) together with the adjacency bit of \(\{i, j\}\) in \(b\).

theorem all_zip_pairs {n : ℕ} {bits : List Bool} (h : bits.length = (pairs n).length)
    (P : ℕ × ℕ → Bool → Bool) :
    ((pairs n).zip bits).all (fun pb => P pb.1 pb.2) = true ↔
      ∀ i j, i < j → j < n → P (i, j) (adjBits n bits i j) = true

Uses 5 · Used by 1

Statement usesAdjacency bit of a vertex pair · Vertex pairs in encoding order

Proof usesLookup in a list of pairs with distinct keys · Membership in the vertex pairs · The vertex pairs are listed without repetition

Used byCharacterization of the CLIQUE verifier

TheoremCharacterization of the CLIQUE verifier#✓fully proved

For a mode \(m\) and bit lists \(x\) and \(w\), the verifier for mode \(m\) accepts input \(x\) with witness \(w\) if and only if there are \(k\), \(n\) and a bit list \(\mathit{bits}\) such that \(x\) is the encoding of the instance \((k, n, \mathit{bits})\), \(\mathit{bits}\) has one bit per pair \((i, j)\) with \(i < j < n\), \(w\) has at least \(n\) bits, exactly \(k\) of the first \(n\) bits of \(w\) are set, and for all \(i < j < n\) the pair condition of \(m\) holds for the bit of the pair \(\{i, j\}\) and the bits \(w_i\) and \(w_j\).

theorem kgCheck_iff (m : Mode) (x w : List Bool) : kgCheck m x w = true ↔
    ∃ k n bits, x = encodeKG k n bits ∧ bits.length = (pairs n).length ∧ n ≤ w.length ∧
      (w.take n).count true = k ∧ ∀ i j, i < j → j < n →
        m.ok (adjBits n bits i j) (w.getD i false) (w.getD j false) = true

Uses 9 · Used by 2

Statement usesModes of the clique verifier · Pair condition of the clique verifier · The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · Adjacency bit of a vertex pair · Encoding of a graph instance · Vertex pairs in encoding order

Proof usesChecking each listed vertex pair against its bit · Decoding a graph instance · Reading a unary length prefix

Used byAn accepted input encodes an instance with a good vertex set · The characteristic vector of a good vertex set is accepted

TheoremCounting the set bits of a list built from a function#✓fully proved

For every natural number \(n\) and every function \(f\) from \(\{0, \dots, n-1\}\) to the Booleans, the number of entries equal to true in the list \(f(0), f(1), \dots, f(n-1)\) equals the number of indices \(i < n\) with \(f(i)\) true.

theorem count_ofFn : ∀ {n : ℕ} (f : Fin n → Bool),
    (List.ofFn f).count true = (Finset.univ.filter fun i => f i = true).card

Used by 2

Used byAn accepted input encodes an instance with a good vertex set · The characteristic vector of a good vertex set is accepted

TheoremThe first \(n\) bits of a list, read index by index#✓fully proved

If a bit list \(w\) has length at least \(n\), then the first \(n\) entries of \(w\) form the list \((w_0, \dots, w_{n-1})\), where \(w_i\) is the entry of \(w\) at index \(i\) (taken as false past the end of \(w\)).

theorem take_eq_ofFn {n : ℕ} {w : List Bool} (hn : n ≤ w.length) :
    w.take n = List.ofFn fun i : Fin n => w.getD i false

Used by 1

Used byAn accepted input encodes an instance with a good vertex set

DefinitionVertex sets meeting a mode's pair condition#✓fully proved

For a mode \(m\), a number \(n\), a list of pair bits and a set \(s\) of vertices in \(\{0, \dots, n - 1\}\), the set \(s\) meets the condition of \(m\) when for all vertices \(i < j\) the pair condition \(\mathrm{ok}_m(b_{ij}, [i \in s], [j \in s])\) holds, where \([i \in s]\) says whether \(i\) is chosen and \(b_{ij}\) is the bit of the pair \(\{i, j\}\): listing the pairs \(i' < j' < n\) in encoding order (rows \(i'\) ascending, within a row \(j'\) descending), the \(t\)-th bit of the list belongs to the \(t\)-th pair, and \(b_{ij}\) is false if the list has no bit for \(\{i, j\}\).

def SetOk (m : Mode) (n : ℕ) (bits : List Bool) (s : Finset (Fin n)) : Prop :=
  ∀ i j : Fin n, i < j → m.ok (adjBits n bits i j) (decide (i ∈ s)) (decide (j ∈ s)) = true

Uses 3 · Used by 6

Statement usesModes of the clique verifier · Pair condition of the clique verifier · Adjacency bit of a vertex pair

Used byCliques of the graph given by pair bits · Vertex covers of the graph given by pair bits · An accepted input encodes an instance with a good vertex set · Independent sets of the graph given by pair bits · The characteristic vector of a good vertex set is accepted · Verifying a graph language defined by a vertex-set condition

TheoremAn accepted input encodes an instance with a good vertex set#✓fully proved

Fix a mode (clique, independent set or vertex cover) and bit strings \(x\) and \(w\). If the verifier in that mode accepts the input \(x\) with witness \(w\), then there are natural numbers \(k\) and \(n\) and a list of bits \(b\) such that \(x\) is the encoding of the instance \((k, n, b)\), \(b\) has exactly one bit per vertex pair \((i, j)\) with \(i < j < n\), and some set of exactly \(k\) of the vertices \(0, \dots, n-1\) meets the mode's pair condition on every pair \(i < j\).

theorem exists_setOk {m : Mode} {x w : List Bool} (h : kgCheck m x w = true) :
    ∃ k n bits, x = encodeKG k n bits ∧ bits.length = (pairs n).length ∧
      ∃ s : Finset (Fin n), s.card = k ∧ SetOk m n bits s

Uses 10 · Used by 1

Statement usesModes of the clique verifier · Vertex sets meeting a mode's pair condition · The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · Encoding of a graph instance · Vertex pairs in encoding order

Proof usesPair condition of the clique verifier · Counting the set bits of a list built from a function · Characterization of the CLIQUE verifier · The first \(n\) bits of a list, read index by index · Adjacency bit of a vertex pair

Used byVerifying a graph language defined by a vertex-set condition

TheoremThe characteristic vector of a good vertex set is accepted#✓fully proved

Let \(m\) be a mode, \(k\) and \(n\) natural numbers, let \(\mathit{bits}\) be a bit list with one bit per pair \((i, j)\), \(i < j < n\), and let \(s\) be a set of \(k\) vertices of \(\{0, \dots, n - 1\}\) that meets the pair condition of \(m\) on every pair \(i < j\). Then the verifier for mode \(m\) accepts the encoding of \((k, n, \mathit{bits})\) with witness the characteristic vector of \(s\): the list of \(n\) bits whose \(i\)-th bit is set if and only if \(i \in s\).

theorem kgCheck_ofFn {m : Mode} {k n : ℕ} {bits : List Bool} (hl : bits.length = (pairs n).length)
    {s : Finset (Fin n)} (hs : s.card = k) (hok : SetOk m n bits s) :
    kgCheck m (encodeKG k n bits) (List.ofFn fun i : Fin n => decide (i ∈ s)) = true

Uses 9 · Used by 1

Statement usesModes of the clique verifier · Vertex sets meeting a mode's pair condition · The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · Encoding of a graph instance · Vertex pairs in encoding order

Proof usesPair condition of the clique verifier · Counting the set bits of a list built from a function · Characterization of the CLIQUE verifier · Adjacency bit of a vertex pair

Used byVerifying a graph language defined by a vertex-set condition

TheoremVerifying a graph language defined by a vertex-set condition#✓fully proved

Let \(m\) be a mode and \(P\) a property of a number \(k\) and a graph on \(n\) vertices. Suppose that for all \(n\), \(k\) and every bit list \(\mathit{bits}\) with one bit per pair \((i, j)\), \(i < j < n\), the property \(P\) holds for \(k\) and the graph given by \(\mathit{bits}\) exactly when some set of \(k\) vertices meets the pair condition of \(m\) on every pair \(i < j\). Then for every bit list \(x\), \(x\) belongs to the language of instances satisfying \(P\) if and only if the verifier for mode \(m\) accepts \(x\) with some witness \(w\) of length \(|w| \le |x|\).

theorem kgDec_iff_exists (m : Mode) (P : ∀ n : ℕ, ℕ → SimpleGraph (Fin n) → Prop)
    (hP : ∀ n k bits, bits.length = (pairs n).length →
      (P n k (toGraph n bits) ↔ ∃ s : Finset (Fin n), s.card = k ∧ SetOk m n bits s))
    (x : List Bool) : kgDec P x = true ↔ ∃ w, w.length ≤ x.length ∧ kgCheck m x w = true

Uses 9 · Used by 3

Statement usesModes of the clique verifier · Vertex sets meeting a mode's pair condition · The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · Language of graph instances with a property · Vertex pairs in encoding order · The graph encoded by pair bits

Proof usesAn accepted input encodes an instance with a good vertex set · The characteristic vector of a good vertex set is accepted · Encoding of a graph instance

Used byCLIQUE is verified with witnesses no longer than the input · INDEPENDENT-SET is verified with witnesses no longer than the input · VERTEX-COVER is verified by the clique verifier in cover mode

TheoremSymmetric relations on increasing pairs#✓fully proved

Let \(n\) be a natural number and \(R\) a relation on \(\{0, \dots, n-1\}\) such that \(R(i, j)\) implies \(R(j, i)\). Then \(R(i, j)\) holds for all \(i \ne j\) if and only if \(R(i, j)\) holds for all \(i < j\).

theorem forall_ne_iff_lt {n : ℕ} {R : Fin n → Fin n → Prop} (hR : ∀ i j, R i j → R j i) :
    (∀ i j, i ≠ j → R i j) ↔ ∀ i j, i < j → R i j

Used by 3

Used byCliques of the graph given by pair bits · Vertex covers of the graph given by pair bits · Independent sets of the graph given by pair bits

TheoremCliques of the graph given by pair bits#✓fully proved

For natural numbers \(n\) and \(k\) and a list of bits \(b\), the graph on the vertices \(0, \dots, n-1\) read off \(b\) has a clique of exactly \(k\) vertices if and only if there is a set \(s\) of exactly \(k\) of these vertices meeting the clique-mode pair condition on every pair \(i < j\): whenever \(i\) and \(j\) both lie in \(s\), the bit of the pair \(\{i, j\}\) in \(b\) is set.

theorem clique_iff (n k : ℕ) (bits : List Bool) : (∃ s, (toGraph n bits).IsNClique k s) ↔
    ∃ s : Finset (Fin n), s.card = k ∧ SetOk .clique n bits s

Uses 7 · Used by 1

Statement usesModes of the clique verifier · Vertex sets meeting a mode's pair condition · The graph encoded by pair bits

Proof usesPair condition of the clique verifier · Symmetric relations on increasing pairs · Adjacency bit of a vertex pair · Vertex pairs in encoding order

Used byCLIQUE is verified with witnesses no longer than the input

TheoremIndependent sets of the graph given by pair bits#✓fully proved

For natural numbers \(n\) and \(k\) and a list of bits \(b\), the graph on the vertices \(0, \dots, n-1\) read off \(b\) has an independent set of exactly \(k\) vertices if and only if there is a set \(s\) of exactly \(k\) of these vertices meeting the independent-set-mode pair condition on every pair \(i < j\): whenever \(i\) and \(j\) both lie in \(s\), the bit of the pair \(\{i, j\}\) in \(b\) is not set.

theorem indep_iff (n k : ℕ) (bits : List Bool) : (∃ s, (toGraph n bits).IsNIndepSet k s) ↔
    ∃ s : Finset (Fin n), s.card = k ∧ SetOk .indep n bits s

Uses 7 · Used by 1

Statement usesModes of the clique verifier · Vertex sets meeting a mode's pair condition · The graph encoded by pair bits

Proof usesPair condition of the clique verifier · Symmetric relations on increasing pairs · Adjacency bit of a vertex pair · Vertex pairs in encoding order

Used byINDEPENDENT-SET is verified with witnesses no longer than the input

TheoremVertex covers of the graph given by pair bits#✓fully proved

For natural numbers \(n\) and \(k\) and a list of bits \(b\), the graph on the vertices \(0, \dots, n-1\) read off \(b\) has a vertex cover of exactly \(k\) vertices if and only if there is a set \(s\) of exactly \(k\) of these vertices meeting the cover-mode pair condition on every pair \(i < j\): whenever the bit of the pair \(\{i, j\}\) in \(b\) is set, \(i\) or \(j\) lies in \(s\).

theorem cover_iff (n k : ℕ) (bits : List Bool) :
    (∃ s : Finset (Fin n), s.card = k ∧ (toGraph n bits).IsVertexCover (s : Set (Fin n))) ↔
      ∃ s : Finset (Fin n), s.card = k ∧ SetOk .cover n bits s

Uses 7 · Used by 1

Statement usesModes of the clique verifier · Vertex sets meeting a mode's pair condition · The graph encoded by pair bits

Proof usesPair condition of the clique verifier · Symmetric relations on increasing pairs · Adjacency bit of a vertex pair · Vertex pairs in encoding order

Used byVERTEX-COVER is verified by the clique verifier in cover mode

TheoremCLIQUE is verified with witnesses no longer than the input#✓fully proved

For every bit string \(x\), \(x\) is in CLIQUE if and only if there is a bit string \(w\) of length at most the length of \(x\) such that the shared CLIQUE / INDEPENDENT-SET / VERTEX-COVER verifier, run in clique mode, accepts the input \(x\) with witness \(w\).

theorem cliqueDec_iff (x : List Bool) :
    cliqueDec x = true ↔ ∃ w, w.length ≤ x.length ∧ kgCheck .clique x w = true

Uses 6 · Used by 1

Statement usesModes of the clique verifier · The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · CLIQUE

Proof usesCliques of the graph given by pair bits · Verifying a graph language defined by a vertex-set condition · Vertex pairs in encoding order

Used byCLIQUE is in NP

TheoremINDEPENDENT-SET is verified with witnesses no longer than the input#✓fully proved

For every bit string \(x\), \(x\) is in INDEPENDENT-SET if and only if there is a bit string \(w\) of length at most the length of \(x\) such that the shared CLIQUE / INDEPENDENT-SET / VERTEX-COVER verifier, run in independent-set mode, accepts the input \(x\) with witness \(w\).

theorem indSetDec_iff (x : List Bool) :
    indSetDec x = true ↔ ∃ w, w.length ≤ x.length ∧ kgCheck .indep x w = true

Uses 6 · Used by 1

Statement usesModes of the clique verifier · The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · INDEPENDENT-SET

Proof usesIndependent sets of the graph given by pair bits · Verifying a graph language defined by a vertex-set condition · Vertex pairs in encoding order

Used byINDEPENDENT-SET is in NP

TheoremVERTEX-COVER is verified by the clique verifier in cover mode#✓fully proved

A bit string \(x\) is in VERTEX-COVER if and only if there is a bit string \(w\), no longer than \(x\), such that the clique-family verifier in vertex-cover mode accepts \(x\) with witness \(w\).

theorem vertexCoverDec_iff (x : List Bool) :
    vertexCoverDec x = true ↔ ∃ w, w.length ≤ x.length ∧ kgCheck .cover x w = true

Uses 6 · Used by 1

Statement usesModes of the clique verifier · The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · The VERTEX-COVER problem

Proof usesVertex covers of the graph given by pair bits · Verifying a graph language defined by a vertex-set condition · Vertex pairs in encoding order

Used byVERTEX-COVER (exact size k) is in NP

InductiveStacks of the CLIQUE verifier#✓fully proved

The verifier machine for CLIQUE, INDEPENDENT-SET and VERTEX-COVER, run on an instance with target size \(k\) and \(n\) vertices, has six stacks: the input \(X\), the witness \(W\), the counter \(C\) (holding \(k\)), the counter \(N\) (holding \(n\)), the vertex stack \(V\) and its scratch stack \(T\).

inductive K | X | W | C | N | V | T
  deriving DecidableEq

Used by 16

Used byRun of the load phase · Load step of the CLIQUE verifier · Program of the clique verifier · The clique verifier's unary reader · Reading an unterminated unary number rejects · The clique verifier's unary reader succeeds · One row of the clique verifier's walk · All rows of the clique verifier's walk · The verifier machine for clique, independent set and vertex cover · One step of a clique-verifier program to a known label · Statements of the clique verifier · Walking the pairs of one row of the clique verifier · Walk step of the clique verifier · Rest of a walk step of the clique verifier · The CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier as a host component · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier

InductiveLabels of the CLIQUE verifier#✓fully proved

On an instance with target size \(k\) and \(n\) vertices, the verifier machine has the labels: read \(k\), read \(n\), load the witness, walk a row (carrying a bit \(c\), the conjunction of the row's pair conditions so far), put the row back, accept, and reject.

inductive Lab | rdK | rdN | load | walk (c : Bool) | back | yes | no
  deriving DecidableEq

Used by 17

Used byRun of the load phase · Load step of the CLIQUE verifier · Program of the clique verifier · The clique verifier's unary reader · Reading an unterminated unary number rejects · The clique verifier's unary reader succeeds · One row of the clique verifier's walk · All rows of the clique verifier's walk · The verifier machine for clique, independent set and vertex cover · One step of a clique-verifier program to a known label · Start label of the clique verifier · Statements of the clique verifier · Walking the pairs of one row of the clique verifier · Walk step of the clique verifier · Rest of a walk step of the clique verifier · The CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier as a host component · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.