Pair bits are read off by position to The row-by-row check of the clique verifier

TheoremPair bits are read off by position#✓fully proved

Let \(n\) be a natural number, and let the pair list of \(n\) be the list of pairs \((i, j)\) with \(i < j < n\) in encoding order. Let \(b\) be a list of bits whose length equals the length of the pair list of \(n\). For all \(i < j < n\), the bit of the pair \((i, j)\) in \(b\) is the entry of \(b\) at the position of \((i, j)\) in the pair list of \(n\).

theorem adjBits_eq_getElem {n : ℕ} {bits : List Bool} {i j : ℕ}
    (h : bits.length = (pairs n).length) (hij : i < j) (hj : j < n) :
    adjBits n bits i j = bits[(pairs n).idxOf (i, j)]'(by
      rw [h]; exact List.idxOf_lt_length_of_mem (mem_pairs.2 ⟨hij, hj⟩))

def pairs (n : ℕ) : List (ℕ × ℕ) :=
  (List.range n).flatMap fun i => ((List.range n).reverse.filter (i < ·)).map (i, ·)

CSLibExt/Computability/Complexity/Karp/Clique.lean:50

def adjBits (n : ℕ) (bits : List Bool) (i j : ℕ) : Bool :=
  (((pairs n).zip bits).lookup (min i j, max i j)).getD false

CSLibExt/Computability/Complexity/Karp/Clique.lean:54

Uses 3 · Used by 3

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

Used byPair bits computed by a function · Complementing the pair bits complements the graph · Vertex covers in terms of the pair bits

TheoremPair bits computed by a function#✓fully proved

Let \(n\) be a natural number, let \(f\) be a function from pairs of natural numbers to bits, and let \(b\) be the list obtained by applying \(f\) to each entry of the pair list of \(n\) (the pairs \((i, j)\) with \(i < j < n\) in encoding order). Then for all \(i < j < n\), the bit of the pair \((i, j)\) in \(b\) is \(f(i, j)\).

theorem adjBits_map_pairs {n i j : ℕ} (f : ℕ × ℕ → Bool) (hij : i < j) (hj : j < n) :
    adjBits n ((pairs n).map f) i j = f (i, j)

def adjBits (n : ℕ) (bits : List Bool) (i j : ℕ) : Bool :=
  (((pairs n).zip bits).lookup (min i j, max i j)).getD false

CSLibExt/Computability/Complexity/Karp/Clique.lean:54

def pairs (n : ℕ) : List (ℕ × ℕ) :=
  (List.range n).flatMap fun i => ((List.range n).reverse.filter (i < ·)).map (i, ·)

CSLibExt/Computability/Complexity/Karp/Clique.lean:50

Uses 4 · Used by 1

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

Proof usesPair bits are read off by position · Membership in the vertex pairs

Used byAdjacency in Karp's clique graph

TheoremComplementing the pair bits complements the graph#✓fully proved

Let \(n \in \mathbb{N}\) and let \(b\) be a list of bits whose length is the number of pairs \((i, j)\) with \(i < j < n\). Then the graph on \(\{0, \dots, n-1\}\) read off the list obtained by negating every bit of \(b\) is the complement of the graph on \(\{0, \dots, n-1\}\) read off \(b\).

theorem toGraph_map_not {n : ℕ} {bits : List Bool} (h : bits.length = (pairs n).length) :
    toGraph n (bits.map not) = (toGraph n bits)ᶜ

def pairs (n : ℕ) : List (ℕ × ℕ) :=
  (List.range n).flatMap fun i => ((List.range n).reverse.filter (i < ·)).map (i, ·)

CSLibExt/Computability/Complexity/Karp/Clique.lean:50

def toGraph (n : ℕ) (bits : List Bool) : SimpleGraph (Fin n) where
  Adj i j := i ≠ j ∧ adjBits n bits i j = true
  symm := ⟨fun i j h => ⟨h.1.symm, by rw [adjBits, min_comm, max_comm]; exact h.2⟩⟩
  loopless := ⟨fun i h => h.1 rfl⟩

CSLibExt/Computability/Complexity/Karp/Clique.lean:58

Uses 5 · Used by 1

Statement usesVertex pairs in encoding order · The graph encoded by pair bits

Proof usesAdjacency bit of a vertex pair · Pair bits are read off by position · Membership in the vertex pairs

Used byCorrectness of the complementing map from CLIQUE to INDEPENDENT-SET

TheoremCorrectness of the complementing map from CLIQUE to INDEPENDENT-SET#✓fully proved

For every bit string \(x\), CLIQUE accepts \(x\) if and only if INDEPENDENT-SET accepts the image of \(x\) under the complementing map from CLIQUE to INDEPENDENT-SET instances.

theorem cliqueDec_eq_indSetDec_flipKG (x : List Bool) : cliqueDec x = indSetDec (flipKG x)

noncomputable def cliqueDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  kgDec fun _ k G => ∃ s, G.IsNClique k s

CSLibExt/Computability/Complexity/Karp/Clique.lean:84

noncomputable def indSetDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  kgDec fun _ k G => ∃ s, G.IsNIndepSet k s

CSLibExt/Computability/Complexity/Karp/Clique.lean:88

def flipKG (x : List Bool) : List Bool :=
  match decodeKG x with
  | some (k, n, bits) => encodeKG k n (bits.map not)
  | none => noKG

CSLibExt/Computability/Complexity/Karp/Clique.lean:119

Uses 13 · Used by 1

Statement usesCLIQUE · Complementing map from CLIQUE to INDEPENDENT-SET instances · INDEPENDENT-SET

Proof usesDecoding a graph instance · Encoding of a graph instance · Language of graph instances with a property · Unparsable input is rejected · Fixed no-instance · Vertex pairs in encoding order · The graph encoded by pair bits · Complementing the pair bits complements the graph · Reading a unary length prefix · Decision problems

Used byINDEPENDENT-SET is NP-hard

TheoremIndependent sets and vertex covers of complementary sizes#✓fully proved

Let \(G\) be a simple graph whose vertices are \(0, 1, \dots, n - 1\), and let \(k \le n\). Then \(G\) has an independent set of exactly \(k\) vertices if and only if \(G\) has a vertex cover of exactly \(n - k\) vertices.

theorem exists_isNIndepSet_iff_exists_isVertexCover {n k : ℕ} (G : SimpleGraph (Fin n))
    (hk : k ≤ n) : (∃ s, G.IsNIndepSet k s) ↔
      ∃ s : Finset (Fin n), s.card = n - k ∧ G.IsVertexCover (s : Set (Fin n))

Used by 1

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

TheoremMembership in the literal occurrences of a CNF formula#✓fully proved

Let \(\varphi\) be a CNF formula with clauses \(C_0, \dots, C_{m-1}\), let \(i\) and \(x\) be natural numbers and let \(b\) be a Boolean. The triple \((i, x, b)\) belongs to the list of literal occurrences of \(\varphi\) if and only if \(i < m\) and the literal \((x, b)\) belongs to \(C_i\).

theorem mem_occs {p : ℕ × ℕ × Bool} {φ : CNF} :
    p ∈ occs φ ↔ ∃ h : p.1 < φ.length, p.2 ∈ φ[p.1]

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def occs (φ : CNF) : List (ℕ × ℕ × Bool) :=
  φ.zipIdx.flatMap fun p => p.1.map fun l => (p.2, l.1, l.2)

CSLibExt/Computability/Complexity/Karp/Clique.lean:97

Uses 3 · Used by 1

Statement usesLiteral occurrences of a CNF formula · CNF formula · CNF clause

Used byKarp's reduction from SAT to CLIQUE is correct

TheoremAdjacency in Karp's clique graph#✓fully proved

Let \(\varphi\) be a CNF formula and let \(o_0, \dots, o_{m-1}\) be its literal occurrences (clause index, variable, polarity) in formula order. In Karp's graph of \(\varphi\), the graph on \(\{0, \dots, m-1\}\) read off the clique pair bits of \(\varphi\), vertices \(i\) and \(j\) are adjacent if and only if \(i \ne j\) and the occurrences \(o_i\) and \(o_j\) are adjacent, that is, they lie in different clauses and are not complementary (they are not the same variable with opposite polarities).

theorem toGraph_cliqueBits_adj {φ : CNF} {i j : Fin (occs φ).length} :
    (toGraph _ (cliqueBits φ)).Adj i j ↔ i ≠ j ∧ occAdj (occs φ)[i] (occs φ)[j] = true

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def occs (φ : CNF) : List (ℕ × ℕ × Bool) :=
  φ.zipIdx.flatMap fun p => p.1.map fun l => (p.2, l.1, l.2)

CSLibExt/Computability/Complexity/Karp/Clique.lean:97

def toGraph (n : ℕ) (bits : List Bool) : SimpleGraph (Fin n) where
  Adj i j := i ≠ j ∧ adjBits n bits i j = true
  symm := ⟨fun i j h => ⟨h.1.symm, by rw [adjBits, min_comm, max_comm]; exact h.2⟩⟩
  loopless := ⟨fun i h => h.1 rfl⟩

CSLibExt/Computability/Complexity/Karp/Clique.lean:58

def cliqueBits (φ : CNF) : List Bool :=
  (pairs (occs φ).length).map fun p => occAdj ((occs φ).getD p.1 (0, 0, false))
    ((occs φ).getD p.2 (0, 0, false))

CSLibExt/Computability/Complexity/Karp/Clique.lean:105

def occAdj (o o' : ℕ × ℕ × Bool) : Bool :=
  o.1 != o'.1 && !(o.2.1 == o'.2.1 && o.2.2 != o'.2.2)

CSLibExt/Computability/Complexity/Karp/Clique.lean:101

Uses 8 · Used by 1

Statement usesAdjacency bits of Karp's clique graph · Adjacency of literal occurrences in Karp's clique graph · Literal occurrences of a CNF formula · The graph encoded by pair bits · CNF formula

Proof usesAdjacency bit of a vertex pair · Pair bits computed by a function · Vertex pairs in encoding order

Used byKarp's reduction from SAT to CLIQUE is correct

TheoremKarp's reduction from SAT to CLIQUE is correct#✓fully proved

A CNF formula \(\varphi\) with \(m\) clauses is satisfiable if and only if Karp's graph of \(\varphi\) has a clique of exactly \(m\) vertices. Karp's graph has one vertex for each literal occurrence of \(\varphi\), and two occurrences are adjacent when they lie in different clauses and are not complementary.

theorem cnfSat_iff_exists_isNClique (φ : CNF) :
    CNFSat φ ↔ ∃ s, (toGraph (occs φ).length (cliqueBits φ)).IsNClique φ.length s

abbrev CNF := List CNFClause

CSLibExt/Logics/Propositional/CNF/Basic.lean:33

def CNFSat (φ : CNF) : Prop :=
  ∃ v : Nat → Bool, ∀ C ∈ φ, ∃ (x : Nat) (b : Bool), (x, b) ∈ C ∧ v x = b

CSLibExt/Logics/Propositional/CNF/Basic.lean:36

def toGraph (n : ℕ) (bits : List Bool) : SimpleGraph (Fin n) where
  Adj i j := i ≠ j ∧ adjBits n bits i j = true
  symm := ⟨fun i j h => ⟨h.1.symm, by rw [adjBits, min_comm, max_comm]; exact h.2⟩⟩
  loopless := ⟨fun i h => h.1 rfl⟩

CSLibExt/Computability/Complexity/Karp/Clique.lean:58

def occs (φ : CNF) : List (ℕ × ℕ × Bool) :=
  φ.zipIdx.flatMap fun p => p.1.map fun l => (p.2, l.1, l.2)

CSLibExt/Computability/Complexity/Karp/Clique.lean:97

def cliqueBits (φ : CNF) : List Bool :=
  (pairs (occs φ).length).map fun p => occAdj ((occs φ).getD p.1 (0, 0, false))
    ((occs φ).getD p.2 (0, 0, false))

CSLibExt/Computability/Complexity/Karp/Clique.lean:105

Uses 9 · Used by 1

Statement usesAdjacency bits of Karp's clique graph · Literal occurrences of a CNF formula · The graph encoded by pair bits · CNF formula · CNF clause · Satisfiability of a CNF formula

Proof usesMembership in the literal occurrences of a CNF formula · Adjacency of literal occurrences in Karp's clique graph · Adjacency in Karp's clique graph

Used byCLIQUE is NP-hard

TheoremSAT decision on undecodable input (moved alias)#✓fully proved

Moved to DenseSAT.ToBinary.satDec_of_decodeCNF_eq_none (DenseToBinary).

@[deprecated DenseSAT.ToBinary.satDec_of_decodeCNF_eq_none (since := "2026-10-15")]
theorem satDec_of_decodeCNF_eq_none {x : List Bool} (h : decodeCNF x = none) :
    satDec x = false

def decodeCNF (input : List Bool) : Option CNF := do
  let (φ, rest) ← decodeCNFAux input
  if rest.isEmpty then some φ else none

CSLibExt/Computability/CookLevin.lean:108

noncomputable def satDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  fun x => if x ∈ SATLang then true else false

CSLibExt/Computability/CookLevin.lean:391

Uses 4

Statement usesDecoding a complete length-prefixed CNF formula · SAT as a decision problem · CNF formula

Proof usesUnparsable input is not in SAT

InductiveModes of the clique verifier#✓fully proved

A mode is one of three values, clique, independent set and vertex cover, naming the three graph problems CLIQUE, INDEPENDENT-SET and VERTEX-COVER that share one NP verifier.

inductive Mode | clique | indep | cover
  deriving DecidableEq

Used by 34

DefinitionPair condition of the clique verifier#✓fully proved

For a mode \(m\), the adjacency bit \(b\) of a vertex pair \(\{i, j\}\), and flags \(s_i\), \(s_j\) saying whether \(i\) and \(j\) are chosen, the pair condition \(\mathrm{ok}_m(b, s_i, s_j)\) is \(\lnot(s_i \land s_j) \lor b\) for clique, \(\lnot(s_i \land s_j) \lor \lnot b\) for independent set, and \(\lnot b \lor s_i \lor s_j\) for vertex cover.

def Mode.ok : Mode → Bool → Bool → Bool → Bool
  | .clique, b, si, sj => !(si && sj) || b
  | .indep, b, si, sj => !(si && sj) || !b
  | .cover, b, si, sj => !b || si || sj

Uses 1 · Used by 12

Statement usesModes of the clique verifier

Used byThe verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · The pair condition splits by vertex · Cliques 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 verifier as a row-by-row check · Characterization of the CLIQUE verifier · The characteristic vector of a good vertex set is accepted · The row-by-row check is the pairwise check · Vertex sets meeting a mode's pair condition · The verifier machine for clique, independent set and vertex cover

DefinitionThe verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER#✓fully proved

For a mode \(m\), an input \(x\) and a witness \(w\) (bit lists), the verifier rejects if \(x\) does not decode to a triple \((k, n, \mathit{bits})\). Otherwise it accepts if and only if \(\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 every pair \((i, j)\), matched with its bit \(b\) in the encoding order of the pairs, the pair condition of \(m\) holds for \(b\), \(w_i\) and \(w_j\). So the first \(n\) bits of \(w\) choose the vertices.

def kgCheck (m : Mode) (x w : List Bool) : Bool :=
  match decodeKG x with
  | none => false
  | some (k, n, bits) => bits.length == (pairs n).length && n ≤ w.length &&
      (w.take n).count true == k &&
      ((pairs n).zip bits).all fun pb => m.ok pb.2 (w.getD pb.1.1 false) (w.getD pb.1.2 false)

inductive Mode | clique | indep | cover
  deriving DecidableEq

CSLibExt/Computability/Complexity/Karp/CliqueVerify.lean:50

def decodeKG (x : List Bool) : Option (ℕ × ℕ × List Bool) := do
  let (k, r) ← readUnaryLength x
  let (n, bits) ← readUnaryLength r
  pure (k, n, bits)

CSLibExt/Computability/Complexity/Karp/Clique.lean:68

def pairs (n : ℕ) : List (ℕ × ℕ) :=
  (List.range n).flatMap fun i => ((List.range n).reverse.filter (i < ·)).map (i, ·)

CSLibExt/Computability/Complexity/Karp/Clique.lean:50

Uses 4 · Used by 10

Statement usesModes of the clique verifier · Pair condition of the clique verifier · Decoding a graph instance · Vertex pairs in encoding order

Used byCLIQUE is verified with witnesses no longer than the input · An accepted input encodes an instance with a good vertex set · INDEPENDENT-SET is verified with witnesses no longer than the input · The verifier as a row-by-row check · Characterization of the CLIQUE verifier · The characteristic vector of a good vertex set is accepted · Verifying a graph language defined by a vertex-set condition · VERTEX-COVER is verified by the clique verifier in cover mode · The verifier machine for clique, independent set and vertex cover · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier

DefinitionVertices that settle their pairs alone#✓fully proved

For a mode and the Boolean saying whether a vertex \(i\) is chosen, the result is true when \(i\) alone settles the condition on every pair \(\{i, j\}\): in the clique and independent-set modes it is true exactly when \(i\) is not chosen, and in the vertex-cover mode exactly when \(i\) is chosen.

def Mode.free : Mode → Bool → Bool
  | .cover, si => si
  | _, si => !si

Uses 1 · Used by 7

Statement usesModes of the clique verifier

Used byThe pair condition splits by vertex · The row-by-row check of the clique verifier · The row-by-row check is the pairwise check · One row of the clique verifier's walk · All rows of the clique verifier's walk · Walking the pairs of one row of the clique verifier · Rest of a walk step of the clique verifier

DefinitionThe pair condition left to the later vertex#✓fully proved

For a mode \(m\), a pair bit \(b\) and a flag \(s_j\) saying whether vertex \(j\) is chosen, \(\mathrm{sat}_m(b, s_j)\) is \(\lnot s_j \lor b\) for clique, \(\lnot s_j \lor \lnot b\) for independent set, and \(\lnot b \lor s_j\) for vertex cover.

It is the pair condition on \(\{i, j\}\) when vertex \(i\) does not settle it.

def Mode.sat : Mode → Bool → Bool → Bool
  | .clique, b, sj => !sj || b
  | .indep, b, sj => !sj || !b
  | .cover, b, sj => !b || sj

Uses 1 · Used by 7

Statement usesModes of the clique verifier

Used byThe pair condition splits by vertex · The row-by-row check of the clique verifier · The row-by-row check is the pairwise check · One row of the clique verifier's walk · All rows of the clique verifier's walk · Walking the pairs of one row of the clique verifier · Rest of a walk step of the clique verifier

TheoremThe pair condition splits by vertex#✓fully proved

For a mode \(m\) and Booleans \(b\), \(s_i\), \(s_j\), let \(\mathrm{ok}_m(b, s_i, s_j)\) be the pair condition of \(m\): \(\lnot(s_i \land s_j) \lor b\) for clique, \(\lnot(s_i \land s_j) \lor \lnot b\) for independent set and \(\lnot b \lor s_i \lor s_j\) for vertex cover. Let \(\mathrm{free}_m(s_i)\), the part that vertex \(i\) alone settles, be \(\lnot s_i\) for clique and independent set and \(s_i\) for vertex cover, and let \(\mathrm{sat}_m(b, s_j)\), the part left to \(j\), be \(\lnot s_j \lor b\) for clique, \(\lnot s_j \lor \lnot b\) for independent set and \(\lnot b \lor s_j\) for vertex cover. Then for every mode \(m\) and all Booleans \(b\), \(s_i\), \(s_j\), we have \(\mathrm{ok}_m(b, s_i, s_j) = \mathrm{free}_m(s_i) \lor \mathrm{sat}_m(b, s_j)\).

theorem Mode.ok_eq (m : Mode) (b si sj : Bool) : m.ok b si sj = (m.free si || m.sat b sj)

Uses 4 · Used by 1

Statement usesModes of the clique verifier · Vertices that settle their pairs alone · Pair condition of the clique verifier · The pair condition left to the later vertex

Used byThe row-by-row check is the pairwise check

TheoremVertex pairs in encoding order for one more vertex#✓fully proved

For a natural number \(m\), write \(P(m)\) for the list of pairs \((i, j)\) of natural numbers with \(i < j < m\), ordered by \(i\) ascending and, for each \(i\), by \(j\) descending. Then for every natural number \(n\), \(P(n + 1)\) is the list \((0, n), (0, n - 1), \dots, (0, 1)\) (empty when \(n = 0\)) followed by the pairs \((i + 1, j + 1)\) for the pairs \((i, j)\) of \(P(n)\), in the order of \(P(n)\).

theorem pairs_succ (n : ℕ) : pairs (n + 1) = (List.range n).reverse.map (fun j => (0, j + 1)) ++
    (pairs n).map fun p => (p.1 + 1, p.2 + 1)

Uses 1 · Used by 2

Statement usesVertex pairs in encoding order

Used byChosen-flag pairs of a list with a new head · Pair bits of an occurrence list, row by row

DefinitionChosen-flag pairs#✓fully proved

For a list \(s = (s_0, \dots, s_{\ell - 1})\) of Booleans, the chosen-flag pairs of \(s\) are the pairs \((s_i, s_j)\), one for each vertex pair \((i, j)\) with \(i < j < \ell\), listed in the encoding order of the vertex pairs of \(\ell\) vertices (rows \(i\) ascending, within a row \(j\) descending).

def pairVals (s : List Bool) : List (Bool × Bool) :=
  (pairs s.length).map fun p => (s.getD p.1 false, s.getD p.2 false)

Uses 1 · Used by 3

Statement usesVertex pairs in encoding order

Used byChosen-flag pairs of a list with a new head · The verifier as a row-by-row check · The row-by-row check is the pairwise check

TheoremReading a list at every index#✓fully proved

For every list \(s\) of Booleans of length \(\ell\), reading \(s\) at the indices \(0, 1, \dots, \ell - 1\) in turn (with default value false) gives back \(s\).

theorem map_getD_range (s : List Bool) : (List.range s.length).map (s.getD · false) = s

Used by 1

Used byChosen-flag pairs of a list with a new head

TheoremChosen-flag pairs of a list with a new head#✓fully proved

For a Boolean \(a\) and a list \(s = (s_0, \dots, s_{\ell - 1})\) of Booleans, the chosen-flag pairs of the list \((a, s_0, \dots, s_{\ell - 1})\) are \((a, s_{\ell - 1}), (a, s_{\ell - 2}), \dots, (a, s_0)\), followed by the chosen-flag pairs of \(s\).

theorem pairVals_cons (a : Bool) (s : List Bool) :
    pairVals (a :: s) = s.reverse.map (a, ·) ++ pairVals s

Uses 4 · Used by 1

Statement usesChosen-flag pairs

Proof usesReading a list at every index · Vertex pairs in encoding order for one more vertex · Vertex pairs in encoding order

Used byThe row-by-row check is the pairwise check

DefinitionThe row-by-row check of the clique verifier#✓fully proved

For a mode \(m\), the row-by-row check of a list of chosen-flags against a list \(b\) of pair bits is defined by recursion on the flags. For the empty list it holds iff \(b\) is empty. For a flag \(a\) followed by the flags \(r\) of the later vertices, write \(\rho\) for the reverse of \(r\): the check holds iff \(|r| \le |b|\), either \(a\) is free for \(m\) or \(\mathrm{sat}_m(b_t, \rho_t)\) holds for every \(t < |r|\) (indices from \(0\)), and the check of \(r\) against \(b\) with its first \(|r|\) bits dropped holds.

This is what the machine checks, vertex by vertex; at the end no bit may be left.

def rowsOk (m : Mode) : List Bool → List Bool → Bool
  | [], bs => bs.isEmpty
  | s :: rest, bs => decide (rest.length ≤ bs.length) &&
      (m.free s || (rest.reverse.zip bs).all fun p => m.sat p.2 p.1) &&
      rowsOk m rest (bs.drop rest.length)

Uses 3 · Used by 4

Statement usesModes of the clique verifier · Vertices that settle their pairs alone · The pair condition left to the later vertex

Used byThe verifier as a row-by-row check · The row-by-row check is the pairwise check · All rows of the clique verifier's walk · The verifier machine for clique, independent set and vertex cover

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.