Statements of the clique verifier to Row-by-row pair bits see only adjacency

AbbreviationStatements of the clique verifier#✓fully proved

The statements of the verifier are those of a multi-stack Turing machine (Mathlib's TM2 model) with the six stacks \(X, W, C, N, V, T\), each over the symbol alphabet of the SAT verifier, the verifier's labels, and one Boolean of local state.

abbrev Stmt := TM2.Stmt (fun _ : K => Sym) Lab Bool

Uses 3 · Used by 6

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Stack alphabet of the SAT verifier

Used byLoad step of the CLIQUE verifier · The clique verifier's unary reader · One step of a clique-verifier program to a known label · 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

DefinitionThe clique verifier's unary reader#✓fully proved

For a stack \(c\) and labels \(\ell\) (its own) and \(\ell'\) (the next), the unary reader onto \(c\) is the verifier statement that inspects the input stack \(X\) and sets the state to whether \(X\) is empty: if it is, it goes to the rejecting label; otherwise it pops the top symbol of \(X\) and sets the state to whether that symbol is the bit \(1\); if so, it pushes the bit \(1\) onto \(c\) and goes to \(\ell\), while any other symbol (normally the terminating \(0\)) sends it to \(\ell'\).

Run from \(\ell\), it reads a unary number off \(X\) onto the counter \(c\).

def readU (c : K) (self next : Lab) : Stmt :=
  .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .no) <|
    .pop .X (fun _ o => bitOf Sym.bit? o) <| .branch id
      (.push c (fun _ => .bit true) (.goto fun _ => self)) (.goto fun _ => next)

Uses 6 · Used by 3

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Statements of the clique verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byProgram of the clique verifier · Reading an unterminated unary number rejects · The clique verifier's unary reader succeeds

DefinitionLoad step of the CLIQUE verifier#✓fully proved

The statement run at the load label. If the counter \(N\) is nonempty, it takes a unit off \(N\), rejects if the witness stack \(W\) is empty, and otherwise pops the top of \(W\) and pushes its bit (false for a non-bit symbol) onto the vertex stack \(V\); if that bit is set it also takes a unit off the counter \(C\), rejecting if \(C\) is empty; then it returns to the load label. If \(N\) is empty, it goes to the walk label with its flag \(c\) (the conjunction of the row's pair conditions so far) set to true when \(C\) is empty, and rejects otherwise.

Started from \(n\) on \(N\) and \(k\) on \(C\), it loads the first \(n\) witness bits onto \(V\), bit \(n - 1\) on top, and rejects if \(W\) runs out or the number of set bits among them is not \(k\).

def loadS : Stmt :=
  .pop .N (fun _ o => o.isSome) <| .branch id
    (.peek .W (fun _ o => o.isNone) <| .branch id (.goto fun _ => .no) <|
      .pop .W (fun _ o => bitOf Sym.bit? o) <| .branch id
        (.push .V (fun _ => .bit true) <| .pop .C (fun _ o => o.isSome) <| .branch id
          (.goto fun _ => .load) (.goto fun _ => .no))
        (.push .V (fun _ => .bit false) <| .goto fun _ => .load))
    (.peek .C (fun _ o => o.isNone) <| .branch id (.goto fun _ => .walk true)
      (.goto fun _ => .no))

Uses 6 · Used by 1

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Statements of the clique verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byProgram of the clique verifier

DefinitionRest of a walk step of the clique verifier#✓fully proved

Write \(\mathrm{free}_m(s)\) for the condition that, in mode \(m\), a vertex with chosen-flag \(s\) settles every pair of its row, and \(\mathrm{sat}_m(b', s')\) for the pair condition on pair bit \(b'\) and later vertex flag \(s'\). In mode \(m\) with row flag \(c\), after a bit \(z\) has been popped off the vertex stack \(V\): if \(V\) is now empty, the machine moves to the put-back label when \(\mathrm{free}_m(z)\) or \(c\) holds, and to the reject label otherwise. If \(V\) is not empty, it pushes \(z\) onto the scratch stack \(T\); then it moves to the reject label if the input stack \(X\) is empty, and otherwise pops the top symbol of \(X\), reads it as a bit \(b\) (a non-bit symbol reads as false), and moves to the walk label with flag \(c \wedge \mathrm{sat}_m(b, z)\).

def walkZ (m : Mode) (c z : Bool) : Stmt :=
  .peek .V (fun _ o => o.isNone) <| .branch id
    (.goto fun _ => if m.free z || c then .back else .no) <|
  .push .T (fun _ => .bit z) <|
  .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .no) <|
  .pop .X (fun _ o => bitOf Sym.bit? o) <| .branch id
    (.goto fun _ => .walk (c && m.sat true z)) (.goto fun _ => .walk (c && m.sat false z))

Uses 9 · Used by 3

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · Vertices that settle their pairs alone · The pair condition left to the later vertex · Statements of the clique verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byAll rows of the clique verifier's walk · Walking the pairs of one row of the clique verifier · Walk step of the clique verifier

DefinitionWalk step of the clique verifier#✓fully proved

In mode \(m\) with row flag \(c\), the walk step looks at the vertex stack \(V\). If \(V\) is empty, it moves to the accept label if the input stack \(X\) is empty and to the reject label otherwise. If \(V\) is not empty, it pops the top symbol of \(V\), reads it as a bit \(z\) (a non-bit symbol reads as false), and continues with the rest of the walk step for \(m\), \(c\) and \(z\).

def walkS (m : Mode) (c : Bool) : Stmt :=
  .peek .V (fun _ o => o.isNone) <| .branch id
    (.peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .yes) (.goto fun _ => .no)) <|
  .pop .V (fun _ o => bitOf Sym.bit? o) <| .branch id (walkZ m c true) (walkZ m c false)

Uses 8 · Used by 1

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · Statements of the clique verifier · Rest of a walk step of the clique verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Bit on top of a stack

Used byProgram of the clique verifier

DefinitionProgram of the clique verifier#✓fully proved

For a mode \(m\) (clique, independent set or vertex cover), the verifier program of mode \(m\) assigns a statement to each label of the verifier: to the label that reads the instance's target size \(k\), the unary reader onto the counter \(C\) with own label this label and next label the label that reads the instance's number \(n\) of vertices; to the label that reads \(n\), the unary reader onto the counter \(N\) with own label this label and next label the load label; to the load label, the load step; to the walk label with flag \(c\), the walk step of mode \(m\) with flag \(c\); to the put-back label, the bit-moving loop from the scratch stack \(T\) to the vertex stack \(V\) that reads name-bit symbols as bits and writes each bit \(b\) as the name bit \(b\), with own label the put-back label and next label the walk label with flag true; and to the accept and reject labels, the statement that halts.

Run from the label that reads \(k\), it parses \(k\) and \(n\), loads the witness and walks the rows.

def prog (m : Mode) : Lab → TM2.Stmt (fun _ : K => Sym) Lab Bool
  | .rdK => readU .C .rdK .rdN
  | .rdN => readU .N .rdN .load
  | .load => loadS
  | .walk c => walkS m c
  | .back => moveB .T .V Sym.bit? Sym.bit .back (.walk true)
  | .yes => .halt
  | .no => .halt

Uses 10 · Used by 9

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · Load step of the CLIQUE verifier · The clique verifier's unary reader · Walk step of the clique verifier · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Flag bit of a machine state · Bit-moving loop

Used byRun of the load phase · 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 · Walking the pairs of one row 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

DefinitionStart label of the clique verifier#✓fully proved

The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER starts at the label that reads the instance's size parameter \(k\) (the number of vertices to choose) in unary off the input stack \(X\) onto the counter \(C\).

def start : Lab := .rdK

Uses 1 · Used by 2

Statement usesLabels of the CLIQUE verifier

Used byThe verifier machine for clique, independent set and vertex cover · NP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier

TheoremOne step of a clique-verifier program to a known label#✓fully proved

Let \(M\) be a program that assigns a verifier statement to each label, \(\ell\) and \(\ell'\) labels, \(v\) a state and \(S\) stack contents. If executing the statement \(M(\ell)\) from state \(v\) and stacks \(S\) ends at label \(\ell'\), then there are a state \(v'\) and stack contents \(S'\) such that \(M\) runs in exactly one step from label \(\ell\) with state \(v\) and stacks \(S\) to label \(\ell'\) with state \(v'\) and stacks \(S'\).

theorem run_one {M : Lab → Stmt} {l l' : Lab} {v : Bool} {S : ∀ _ : K, List Sym}
    (h : (TM2.stepAux (M l) v S).l = some l') :
    ∃ v' S', Run M 1 ⟨some l, v, S⟩ ⟨some l', v', S'⟩

Uses 6 · Used by 4

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Statements of the clique verifier · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label

Used byRun of the load phase · Reading an unterminated unary number rejects · All rows of the clique verifier's walk · Walking the pairs of one row of the clique verifier

TheoremThe clique verifier's unary reader succeeds#✓fully proved

Let \(m\) be a mode, \(c\) a stack other than the input stack \(X\), and \(\ell\), \(\ell'\) labels such that the verifier program of mode \(m\) runs, at label \(\ell\), the unary reader onto \(c\) with own label \(\ell\) and next label \(\ell'\). Let \(k, j \in \mathbb{N}\), let \(r\) be a list of bits, \(v\) a state and \(S\) stack contents in which \(X\) holds, from the top, \(k\) ones, then a zero, then the bits of \(r\), and \(c\) holds exactly \(j\) copies of the bit \(1\). Then there are a state \(v'\) and stack contents \(S'\) such that the program runs in exactly \(k + 1\) steps from label \(\ell\) with state \(v\) and stacks \(S\) to label \(\ell'\) with state \(v'\) and stacks \(S'\), where in \(S'\) the stack \(X\) holds the bits of \(r\), the stack \(c\) holds exactly \(k + j\) copies of the bit \(1\), and every stack other than \(X\) and \(c\) is as in \(S\).

theorem readU_some {c : K} {self next : Lab} (hp : prog m self = readU c self next)
    (hc : c ≠ .X) : ∀ (k j : ℕ) (r : List Bool) (v : Bool) (St : ∀ _ : K, List Sym),
      St .X = (List.replicate k true ++ false :: r).map Sym.bit → St c = cnt (Sym.bit true) j →
      ∃ v' S', Run (prog m) (k + 1) ⟨some self, v, St⟩ ⟨some next, v', S'⟩ ∧
        S' .X = r.map Sym.bit ∧ S' c = cnt (Sym.bit true) (k + j) ∧
        ∀ q, q ≠ .X → q ≠ c → S' q = St q

Uses 10 · Used by 1

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · Program of the clique verifier · The clique verifier's unary reader · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesReading a symbol as a name bit · A single step executes the statement at the current label

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

TheoremReading an unterminated unary number rejects#✓fully proved

Let \(m\) be a mode, \(c\) a stack other than the input stack \(X\), and \(\lambda\), \(\mu\) labels such that the verifier for \(m\) runs at \(\lambda\) the unary reader onto \(c\) that loops at \(\lambda\) and exits to \(\mu\). Let \(l\) be a list of Booleans from which no unary length can be read (it contains no false). Then for every machine variable \(v\) and all stack contents in which \(X\) holds exactly the bits of \(l\), the verifier for \(m\) goes from label \(\lambda\) to the rejecting label no in at most \(|l| + 1\) steps.

theorem readU_none {c : K} {self next : Lab} (hp : prog m self = readU c self next)
    (hc : c ≠ .X) : ∀ (l : List Bool) (v : Bool) (St : ∀ _ : K, List Sym),
      readUnaryLength l = none → St .X = l.map Sym.bit →
      ∃ v' S', RunLe (prog m) (l.length + 1) ⟨some self, v, St⟩ ⟨some .no, v', S'⟩

Uses 13 · Used by 1

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · Program of the clique verifier · The clique verifier's unary reader · Stack alphabet of the SAT verifier · Reading a unary length prefix · Runs within a step budget

Proof usesOne step of a clique-verifier program to a known label · Reading a symbol as a name bit · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack

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

TheoremRun of the load phase#✓fully proved

Let \(m\) be a mode, \(n\) and \(j\) natural numbers and \(w\) and \(\mathit{acc}\) bit lists. Start the verifier for mode \(m\) at the load label, in any internal state, with \(n\) in unary on the counter \(N\), \(j\) in unary on the counter \(C\), \(w\) on the witness stack \(W\) and \(\mathit{acc}\) on the vertex stack \(V\). Then within at most \(n + 1\) steps the machine reaches the walk label with its flag \(c\) (the conjunction of the row's pair conditions so far) set to true if \(w\) has at least \(n\) bits and exactly \(j\) of its first \(n\) bits are set, and the reject label otherwise. In the first case \(V\) then holds the first \(n\) bits of \(w\), bit \(n - 1\) on top, above \(\mathit{acc}\), and the stacks \(X\) and \(T\) are unchanged.

theorem load_run : ∀ (n : ℕ) (w acc : List Bool) (j : ℕ) (v : Bool) (St : ∀ _ : K, List Sym),
    St .N = cnt (Sym.bit true) n → St .W = w.map Sym.bit → St .C = cnt (Sym.bit true) j →
    St .V = acc.map Sym.bit →
    ∃ v' S', RunLe (prog m) (n + 1) ⟨some .load, v, St⟩
      ⟨some (if n ≤ w.length ∧ (w.take n).count true = j then .walk true else .no), v', S'⟩ ∧
      (n ≤ w.length ∧ (w.take n).count true = j →
        S' .V = ((w.take n).reverse ++ acc).map Sym.bit ∧ S' .X = St .X ∧ S' .T = St .T)

Uses 12 · Used by 1

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · Program of the clique verifier · Stack alphabet of the SAT verifier · Runs within a step budget · Unary counter

Proof usesOne step of a clique-verifier program to a known label · Reading a symbol as a name bit · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack

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

TheoremWalking the pairs of one row of the clique verifier#✓fully proved

Let \(m\) be a mode and \(s\) a bit. Let \(z = (z_0, \dots, z_{r-1})\) and \(b = (b_0, \dots, b_{q-1})\) be lists of bits, \(c\) a bit, \(v\) a state and \(S\) stack contents in which the vertex stack \(V\) holds, from the top, the name bits \(z_0, \dots, z_{r-1}\) followed by the name bit \(s\), and the input stack \(X\) holds, from the top, the name bits \(b_0, \dots, b_{q-1}\). Then there are a state \(v'\) and stack contents \(S'\) such that within at most \(r + 1\) steps the verifier program of mode \(m\) goes from the walk label with flag \(c\), state \(v\) and stacks \(S\) to state \(v'\) and stacks \(S'\) at the put-back label if \(r \le q\) and either \(\mathrm{free}_m(s)\) holds (a vertex with chosen-flag \(s\) settles its pairs alone) or both \(c\) and \(\mathrm{sat}_m(b_t, z_t)\) for every \(t < r\) hold (the pair condition left to the later vertex, with pair bit \(b_t\) and later-vertex flag \(z_t\)), and at the reject label otherwise. Moreover, if \(r \le q\), then in \(S'\) the stack \(V\) is empty, the scratch stack \(T\) holds \(z_{r-1}, \dots, z_0\) from the top above its contents in \(S\), and \(X\) holds, from the top, \(b_r, \dots, b_{q-1}\).

theorem walkRow_run (si : Bool) : ∀ (zs : List Bool) (c : Bool) (bs : List Bool) (v : Bool)
    (St : ∀ _ : K, List Sym), St .V = (zs ++ [si]).map Sym.bit → St .X = bs.map Sym.bit →
    ∃ v' S', RunLe (prog m) (zs.length + 1) ⟨some (.walk c), v, St⟩
      ⟨some (if zs.length ≤ bs.length ∧
        (m.free si || (c && (zs.zip bs).all fun p => m.sat p.2 p.1)) = true
        then .back else .no), v', S'⟩ ∧
      (zs.length ≤ bs.length → S' .V = [] ∧ S' .T = zs.reverse.map Sym.bit ++ St .T ∧
        S' .X = (bs.drop zs.length).map Sym.bit)

Uses 15 · Used by 1

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · Vertices that settle their pairs alone · The pair condition left to the later vertex · Program of the clique verifier · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesStatements of the clique verifier · One step of a clique-verifier program to a known label · Rest of a walk step of the clique verifier · Reading a symbol as a name bit · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack

Used byOne row of the clique verifier's walk

TheoremOne row of the clique verifier's walk#✓fully proved

Let \(m\) be a mode, \(s_i\) a bit, \(r\) and \(b\) lists of bits, \(v\) a state and \(S\) stack contents in which the vertex stack \(V\) holds, from the top, the bits of the reverse \(\rho\) of \(r\) followed by \(s_i\), the scratch stack \(T\) is empty, and the input stack \(X\) holds the bits \(b\). Call the row condition: \(|r| \le |b|\), and either \(s_i\) is free for \(m\) or \(\mathrm{sat}_m(b_t, \rho_t)\) holds for every \(t < |r|\) (indices from \(0\)). Then there are a state \(v'\) and stack contents \(S'\) such that within at most \(2|r| + 2\) steps the verifier program of mode \(m\) goes from label walk(true) with state \(v\) and stacks \(S\) to state \(v'\) and stacks \(S'\) at label walk(true) if the row condition holds and at the rejecting label otherwise; and if the row condition holds, then in \(S'\) the stack \(V\) holds the bits of \(\rho\), \(T\) is empty, and \(X\) holds \(b\) with its first \(|r|\) bits dropped.

theorem row_run (si : Bool) (rest bs : List Bool) (v : Bool) (St : ∀ _ : K, List Sym)
    (hV : St .V = (rest.reverse ++ [si]).map Sym.bit) (hT : St .T = [])
    (hX : St .X = bs.map Sym.bit) :
    ∃ v' S', RunLe (prog m) (2 * rest.length + 2) ⟨some (.walk true), v, St⟩
      ⟨some (if rest.length ≤ bs.length ∧
        (m.free si || (rest.reverse.zip bs).all fun p => m.sat p.2 p.1) = true
        then .walk true else .no), v', S'⟩ ∧
      (rest.length ≤ bs.length ∧
        (m.free si || (rest.reverse.zip bs).all fun p => m.sat p.2 p.1) = true →
        S' .V = rest.reverse.map Sym.bit ∧ S' .T = [] ∧
          S' .X = (bs.drop rest.length).map Sym.bit)

Uses 13 · Used by 1

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · Vertices that settle their pairs alone · The pair condition left to the later vertex · Program of the clique verifier · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesWalking the pairs of one row of the clique verifier · Reading a symbol as a name bit · Flag bit of a machine state · Exact-length runs of a TM2 machine · Running the bit-moving loop

Used byAll rows of the clique verifier's walk

TheoremAll rows of the clique verifier's walk#✓fully proved

Let \(m\) be a mode, \(r\) and \(b\) lists of bits, \(v\) a state and \(S\) stack contents in which the vertex stack \(V\) holds, from the top, the bits of the reverse of \(r\) (so the last entry of \(r\) is on top), the scratch stack \(T\) is empty, and the input stack \(X\) holds the bits \(b\). Then there are a state \(v'\) and stack contents \(S'\) such that within at most \(|r|(2|r| + 2) + 1\) steps the verifier program of mode \(m\) goes from label walk(true) with state \(v\) and stacks \(S\) to state \(v'\) and stacks \(S'\) at the accepting label if the row-by-row check of \(r\) against \(b\) holds for \(m\), and at the rejecting label otherwise.

theorem rows_run : ∀ (rs bs : List Bool) (v : Bool) (St : ∀ _ : K, List Sym),
    St .V = rs.reverse.map Sym.bit → St .T = [] → St .X = bs.map Sym.bit →
    ∃ v' S', RunLe (prog m) (rs.length * (2 * rs.length + 2) + 1) ⟨some (.walk true), v, St⟩
      ⟨some (if rowsOk m rs bs then .yes else .no), v', S'⟩

Uses 15 · Used by 1

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · Program of the clique verifier · The row-by-row check of the clique verifier · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesVertices that settle their pairs alone · The pair condition left to the later vertex · One row of the clique verifier's walk · One step of a clique-verifier program to a known label · Rest of a walk step of the clique verifier · Reading a symbol as a name bit · Exact-length runs of a TM2 machine · Bit on top of a stack

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

TheoremThe verifier machine for clique, independent set and vertex cover#✓fully proved

Let \(m\) be a mode, \(x\) and \(w\) lists of bits, \(v\) a state and \(S\) stack contents in which the input stack \(X\) holds the bits of \(x\), the witness stack \(W\) holds the bits of \(w\), and every other stack is empty. Then there are a state \(v'\) and stack contents \(S'\) such that within at most \(8(|x| + |w| + 1)^3\) steps the verifier program of mode \(m\) goes from the start label with state \(v\) and stacks \(S\) to state \(v'\) and stacks \(S'\) at the accepting label if the verifier check of mode \(m\) accepts \(x\) with witness \(w\), and at the rejecting label otherwise.

theorem run (m : Mode) (x w : List Bool) (v : Bool) (St : ∀ _ : K, List Sym)
    (hX : St .X = x.map Sym.bit) (hW : St .W = w.map Sym.bit)
    (h0 : ∀ k, k ≠ .X → k ≠ .W → St k = []) :
    ∃ v' S', RunLe (prog m) (8 * (x.length + w.length + 1) ^ 3) ⟨some start, v, St⟩
      ⟨some (if kgCheck m x w then .yes else .no), v', S'⟩

Uses 21 · Used by 1

Statement usesStacks of the CLIQUE verifier · Labels of the CLIQUE verifier · Modes of the clique verifier · The verifier for CLIQUE, INDEPENDENT-SET and VERTEX-COVER · Program of the clique verifier · Start label of the clique verifier · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesPair condition of the clique verifier · The verifier as a row-by-row check · Run of the load phase · Reading an unterminated unary number rejects · The clique verifier's unary reader succeeds · The row-by-row check of the clique verifier · All rows of the clique verifier's walk · Decoding a graph instance · Encoding of a graph instance · Vertex pairs in encoding order · Reading a unary length prefix · Exact-length runs of a TM2 machine · Unary counter

Used byNP membership from the CLIQUE, INDEPENDENT-SET and VERTEX-COVER verifier

TheoremDistinctness of CLIQUE verifier pairs (moved alias)#✓fully proved

Moved to Cslib.Complexity.Karp.pairs_nodup (Karp.CliqueCorrect).

@[deprecated Karp.pairs_nodup (since := "2026-10-15")]
theorem pairs_nodup (n : ℕ) : (pairs n).Nodup

Uses 2

Statement usesVertex pairs in encoding order

Proof usesThe vertex pairs are listed without repetition

DefinitionKarp adjacency of two literals#✓fully proved

For literals \(l = (x, p)\) and \(l' = (x', q)\), each a variable \(x, x' \in \mathbb{N}\) with a polarity \(p, q \in \{\mathrm{true}, \mathrm{false}\}\), the adjacency bit of \(l\) and \(l'\) is false when they are complementary, that is \(x = x'\) and \(p \ne q\), and true otherwise. It is the adjacency of two occurrences in different clauses in Karp's graph.

def adjL (l l' : ℕ × Bool) : Bool := !(l.1 == l'.1 && l.2 != l'.2)

Used by 3

Used byPair bits of a leading clause · Bits pushed by a walk of the CLIQUE emitter · Walk over the occurrence stack in the CLIQUE emitter

DefinitionRow-by-row pair bits of an occurrence list#✓fully proved

For a list of literal occurrences (clause index, variable, polarity), the row-by-row pair bits are defined recursively: the empty list has none, and for a list \(o, o_1, \dots, o_k\) they are the adjacency bits of \(o\) with \(o_k, \dots, o_1\), in that order, followed by the row-by-row pair bits of \(o_1, \dots, o_k\). Two occurrences are adjacent when they lie in different clauses and are not complementary.

def bitsRec : List (ℕ × ℕ × Bool) → List Bool
  | [] => []
  | o :: os => (os.map (occAdj o)).reverse ++ bitsRec os

Uses 1 · Used by 4

Statement usesAdjacency of literal occurrences in Karp's clique graph

Used byRow-by-row pair bits see only adjacency · Pair bits of an occurrence list, row by row · Pair bits of a leading clause · The CLIQUE emitter's row bits are Karp's pair bits

TheoremPair bits of an occurrence list, row by row#✓fully proved

Let \(o_0, \dots, o_{m-1}\) be a list of literal occurrences (clause index, variable, polarity). The list of adjacency bits of \(o_i\) and \(o_j\) over the pairs \((i, j)\) with \(i < j < m\) in encoding order (rows \(i\) ascending, and \(j\) descending within a row) equals the recursive pair bits of the list, which are empty for the empty list and otherwise are the adjacency bits of \(o_0\) with \(o_{m-1}, o_{m-2}, \dots, o_1\), in this order, followed by the recursive pair bits of \(o_1, \dots, o_{m-1}\). Two occurrences are adjacent when they lie in different clauses and are not complementary.

theorem pairBits_eq (os : List (ℕ × ℕ × Bool)) :
    (pairs os.length).map (fun p => occAdj (os.getD p.1 (0, 0, false))
      (os.getD p.2 (0, 0, false))) = bitsRec os

Uses 4 · Used by 1

Statement usesRow-by-row pair bits of an occurrence list · Adjacency of literal occurrences in Karp's clique graph · Vertex pairs in encoding order

Proof usesVertex pairs in encoding order for one more vertex

Used byThe CLIQUE emitter's row bits are Karp's pair bits

TheoremRow-by-row pair bits see only adjacency#✓fully proved

Call two literal occurrences (clause index, variable, polarity) adjacent when they lie in different clauses and are not complementary. Let \(f\) be a map on occurrences such that \(f(a)\) and \(f(b)\) are adjacent exactly when \(a\) and \(b\) are, for all occurrences \(a\) and \(b\). Then for every list of occurrences \(o_1, \dots, o_k\), the row-by-row pair bits of \(f(o_1), \dots, f(o_k)\) equal those of \(o_1, \dots, o_k\).

theorem bitsRec_map (f : ℕ × ℕ × Bool → ℕ × ℕ × Bool)
    (hf : ∀ a b, occAdj (f a) (f b) = occAdj a b) (os : List (ℕ × ℕ × Bool)) :
    bitsRec (os.map f) = bitsRec os

Uses 2 · Used by 1

Statement usesRow-by-row pair bits of an occurrence list · Adjacency of literal occurrences in Karp's clique graph

Used byThe CLIQUE emitter's row bits are Karp's pair bits

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.