Clique emitter: comparing two names to Pair-bit transform of each mode

TheoremClique emitter: comparing two names#✓fully proved

Let \(p\), \(q\) and \(v\) be Booleans, \(u\) and \(w\) lists of bits, \(t\), \(e\) and \(R\) stack-symbol lists with \(R\) empty or not starting with a name bit, \(o\) a list of bits and \(c, n \in \mathbb{N}\). Let \(b\) be \((p = q)\) if \(u = w\) and true otherwise. For some flag \(v'\), the emitter machine goes in at most \(3|w| + 4\) steps from label \(\mathrm{cmp}(p, q)\) with flag \(v\) and the state with token stack \(t\), output \(o\), name stack \(u\), walked stack \(w\) followed by \(R\), walk side \(e\), clause count \(c\), occurrence count \(n\) and empty scratch stacks to label \(\mathrm{mvN}(p, \mathrm{true})\) with flag \(v'\) and the same state except that the output is \(b\) followed by \(o\). Here \(u\) and \(w\) lie on the stacks as name-bit symbols.

theorem cmp_run (p q : Bool) (u w : List Bool) (R : List Sym)
    (hR : R.head?.bind Sym.bit? = none) :
    ∃ v', RunLe prog (3 * w.length + 4)
      ⟨some (.cmp p q), v, st t o (u.map Sym.bit) (w.map Sym.bit ++ R) e c n⟩
      ⟨some (.mvN p true), v', st t ((if u = w then p == q else true) :: o) (u.map Sym.bit)
        (w.map Sym.bit ++ R) e c n⟩

Uses 15 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · The CLIQUE emitter machine · Configuration stacks of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Runs within a step budget

Proof usesFour pairwise distinct stacks · Flag bit of a machine state · Bit blocks · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Correctness of the bit-block comparison · Restoring a stack after a comparison

Used byWalk over the occurrence stack in the CLIQUE emitter

TheoremCLIQUE emitter: putting the current occurrence on the walked stack#✓fully proved

Stacks are listed top first. Let \(p\) be a Boolean, \(u\) a list of Booleans and \(\bar u\) the list of bit symbols \(\mathrm{bit}(b)\) for \(b\) in \(u\), let \(v\) be a flag, \(t\), \(d\), \(e\) lists of symbols, \(o\) a list of Booleans and \(c, n \in \mathbb{N}\). Started at label \(\mathrm{put}(p)\) with flag \(v\), stacks \(T\), \(O\), \(A\), \(D\), \(E\) holding \(t\), \(o\), \(\bar u\), \(d\), \(e\), empty scratch stacks \(B\) and \(X\), and \(c\) and \(n\) clause markers on the counters \(C\) and \(N\), the CLIQUE emitter reaches, in exactly \(2|u| + 3\) steps and with some flag, the label \(\mathrm{lits}\) with \(A\) empty, \(D\) holding the literal marker \(\mathrm{lit}(p)\) on top of \(\bar u\) on top of \(d\), and all other stacks as before.

The name goes from \(A\) to \(D\) through \(B\), so it is reversed twice.

theorem put_run (p : Bool) (u : List Bool) :
    ∃ v', Run prog (2 * u.length + 3) ⟨some (.put p), v, st t o (u.map Sym.bit) d e c n⟩
      ⟨some .lits, v', st t o [] (.lit p :: (u.map Sym.bit ++ d)) e c n⟩

Uses 12 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · The CLIQUE emitter machine · Configuration stacks of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesReading a symbol as a name bit · Flag bit of a machine state · Bit blocks · A single step executes the statement at the current label · Running the bit-moving loop

Used byEmitter run over one literal occurrence

TheoremClique emitter: moving the walk side back#✓fully proved

Let \(p\) and \(v\) be Booleans, \(t\), \(a\) and \(d\) stack-symbol lists, \(o\) a list of bits, \(c, n \in \mathbb{N}\), and let \(L\) be a list of stack symbols each of which is a name bit, a polarity marker or a clause marker. From label \(\mathrm{back}(p)\) with flag \(v\) and the state with token stack \(t\), output \(o\), name stack \(a\), walked stack \(d\), walk side \(L\), clause count \(c\), occurrence count \(n\) and empty scratch stacks, the emitter machine reaches in exactly \(|L| + 1\) steps, for some flag \(v'\), label \(\mathrm{put}(p)\) with flag \(v'\) and the same state except that the walked stack is the reverse of \(L\) followed by \(d\) and the walk side is empty.

theorem back_run (p : Bool) :
    ∀ (L : List Sym), (∀ s ∈ L, isTok s = true) → ∀ (d : List Sym) (v : Bool),
      ∃ v', Run prog (L.length + 1) ⟨some (.back p), v, st t o a d L c n⟩
        ⟨some (.put p), v', st t o a (L.reverse ++ d) [] c n⟩

Uses 10 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · Tokens moved by the walk · The CLIQUE emitter machine · Configuration stacks of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesLiteral-marker test of the 3SAT emitter · A single step executes the statement at the current label

Used byEmitter run over one literal occurrence

TheoremClique emitter: the instance prefix#✓fully proved

Let \(v\) be a Boolean, \(d\) and \(e\) stack-symbol lists, \(o\) a list of bits and \(c, n \in \mathbb{N}\). From label fin with flag \(v\) and the state with empty token stack, output \(o\), empty name stack, walked stack \(d\), walk side \(e\), clause count \(c\), occurrence count \(n\) and empty scratch stacks, the emitter machine reaches in exactly \(n + c + 4\) steps label done with some flag and some state whose output, read top-down, is \(c\) ones, false, \(n\) ones, false, then \(o\).

theorem fin_run :
    ∃ v' S', Run prog (n + c + 4) ⟨some .fin, v, st [] o [] d e c n⟩ ⟨some .done, v', S'⟩ ∧
      S' .O = List.replicate c true ++ false :: (List.replicate n true ++ false :: o)

Uses 14 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · The CLIQUE emitter machine · Configuration stacks of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesRepeating a single bit · Flag bit of a machine state · A single step executes the statement at the current label · Unary counter · Pushing a list of symbols onto one stack · Repeated block · Draining a counter while prepending a block

Used byThe CLIQUE emitter computes Karp's instance in cubic time

TheoremReversing a list preserves the length of a flat map#✓fully proved

Let \(\alpha\) and \(\beta\) be types, \(l\) a list of elements of \(\alpha\) and \(f\) a function from \(\alpha\) to lists of elements of \(\beta\). Concatenating the lists \(f(a)\) for \(a\) running through the reverse of \(l\) gives a list of the same length as concatenating them for \(a\) running through \(l\).

theorem flatMap_reverse_length {α β : Type} (l : List α) (f : α → List β) :
    (l.reverse.flatMap f).length = (l.flatMap f).length

Used by 2

Used byEmitter run over a formula's clauses · The CLIQUE emitter computes Karp's instance in cubic time

TheoremWalk over the occurrence stack in the CLIQUE emitter#✓fully proved

Let \(l = (x, p)\) be a literal occurrence, \(ds\) a list of items (literal occurrences or clause markers), \(f\) and \(v\) Booleans, \(t\) a token stack, \(o\) an output stack of bits, \(e\) a stack of token symbols and \(c, n \in \mathbb{N}\). Let \(D\) be the concatenation of the tokens of the items of \(ds\): a clause marker for a clause marker, and the polarity marker of \(l'\) above the name bits of \(l'\) (the binary encoding of its name as bit symbols) for an occurrence \(l'\). Start the CLIQUE emitter at label \(\mathsf{walk}(p, f)\) with internal variable \(v\), on the configuration stacks with token stack \(t\), output \(o\), name stack the name bits of \(x\), walked-occurrence stack \(D\), other walk stack \(e\) and counts \(c\) and \(n\). Then for some Boolean \(v'\) the machine reaches, in at most \(6\,|D| + 1\) steps, label \(\mathsf{back}(p)\) with internal variable \(v'\) on the configuration stacks with token stack \(t\), output stack the reverse of \(\mathrm{walkBits}(l, f, ds)\) followed by \(o\), name stack the name bits of \(x\), empty walked-occurrence stack, other walk stack the reverse of \(D\) followed by \(e\), and counts \(c\) and \(n\).

theorem walk_run (l : ℕ × Bool) (t : List Sym) (c n : ℕ) :
    ∀ (ds : List (Option (ℕ × Bool))) (f : Bool) (o : List Bool) (e : List Sym) (v : Bool),
      ∃ v', RunLe prog (6 * (ds.flatMap itemTok).length + 1)
        ⟨some (.walk l.2 f), v, st t o (name l.1) (ds.flatMap itemTok) e c n⟩
        ⟨some (.back l.2), v', st t ((walkBits l f ds).reverse ++ o) (name l.1) []
          ((ds.flatMap itemTok).reverse ++ e) c n⟩

Uses 17 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · Tokens of an item on the walked stack · Name bits of a variable in the CLIQUE emitter · The CLIQUE emitter machine · Configuration stacks of the CLIQUE emitter · Bits pushed by a walk of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesKarp adjacency of two literals · Clique emitter: comparing two names · Moving a walked name from \(D\) to \(E\) · Reading a symbol as a name bit · The binary code of natural numbers is injective · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byEmitter run over one literal occurrence

TheoremEmitter run over one literal occurrence#✓fully proved

Write \(\langle \ell, v \mid t, o, a, d, e, c, n\rangle\) for the configuration of the SAT-to-CLIQUE emitter at label \(\ell\) with local bit \(v\), stacks \(T = t\), \(O = o\), \(A = a\), \(D = d\), \(E = e\), empty scratch stacks \(B\) and \(X\), and \(c\) and \(n\) marks on the counters \(C\) and \(N\); juxtaposition of lists is concatenation. Let \(l = (x, p)\) be a literal, \(R\) a list of symbols that is empty or does not start with a name-bit symbol, \(I\) a list of items, \(o\) a list of bits, \(c, n \in \mathbb{N}\) and \(v\) a bit. Let \(\delta\) be the concatenation of the tokens of the items of \(I\), \(\lambda\) the token list of \(l\) as it lies on the token stack, \(\rho\) the reverse of the walk bits of \(l\) with flag false over \(I\), and \(\delta'\) the concatenation of the tokens of the item \(l\) followed by those of \(I\). Then for some bit \(v'\) the machine goes in at most \(7|\delta| + 3|\mathrm{enc}(x)| + 7\) steps, where \(\mathrm{enc}(x)\) is the binary encoding of \(x\), from \(\langle \mathsf{lits}, v \mid \lambda R, o, [], \delta, [], c, n\rangle\) to \(\langle \mathsf{lits}, v' \mid R, \rho\, o, [], \delta', [], c, n + 1\rangle\).

theorem lit_run (l : ℕ × Bool) (R : List Sym) (hR : R.head?.bind Sym.bit? = none)
    (ds : List (Option (ℕ × Bool))) (o : List Bool) (c n : ℕ) (v : Bool) :
    ∃ v', RunLe prog (7 * (ds.flatMap itemTok).length + 3 * (encodeNat l.1).length + 7)
      ⟨some .lits, v, st (Check.litRev l ++ R) o [] (ds.flatMap itemTok) [] c n⟩
      ⟨some .lits, v', st R ((walkBits l false ds).reverse ++ o) []
        ((some l :: ds).flatMap itemTok) [] c (n + 1)⟩

Uses 19 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · Tokens of an item on the walked stack · The CLIQUE emitter machine · Configuration stacks of the CLIQUE emitter · Bits pushed by a walk of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · A literal's tokens on the token stack · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Runs within a step budget

Proof usesClique emitter: moving the walk side back · Tokens moved by the walk · Name bits of a variable in the CLIQUE emitter · CLIQUE emitter: reading a variable name · CLIQUE emitter: putting the current occurrence on the walked stack · Walk over the occurrence stack in the CLIQUE emitter · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byEmitter run over a clause's literals

TheoremEmitter run over a clause's literals#✓fully proved

Write \(\langle \ell, v \mid t, o, a, d, e, c, n\rangle\) for the configuration of the SAT-to-CLIQUE emitter at label \(\ell\) with local bit \(v\), stacks \(T = t\), \(O = o\), \(A = a\), \(D = d\), \(E = e\), empty scratch stacks \(B\) and \(X\), and \(c\) and \(n\) marks on the counters \(C\) and \(N\); juxtaposition of lists is concatenation. Let \(L, c \in \mathbb{N}\), let \(I\) be a list of items and \(\delta\) the concatenation of their tokens, let \(l_1, \dots, l_k\) be literals, \(R\) a list of symbols that is empty or does not start with a name-bit symbol, \(o\) a list of bits, \(n \in \mathbb{N}\) and \(v\) a bit. Let \(\lambda_i\) be the token list of \(l_i\) as it lies on the token stack and \(\Lambda = |\lambda_1| + \dots + |\lambda_k|\). If \(\Lambda + |\delta| \le L\), then for some bit \(v'\) the machine goes in at most \(\Lambda (7L + 7)\) steps from \(\langle \mathsf{lits}, v \mid \lambda_k \cdots \lambda_1 R, o, [], \delta, [], c, n\rangle\) to \(\langle \mathsf{lits}, v' \mid R, \rho\, o, [], \delta', [], c, n + k\rangle\), where \(\rho\) is the rows pushed for the literals \(l_1, \dots, l_k\) above the items \(I\) and \(\delta'\) is the concatenation of the tokens of the items \(l_1, \dots, l_k\) followed by those of \(I\).

theorem lits_run (Lb : ℕ) (ds : List (Option (ℕ × Bool))) (c : ℕ) :
    ∀ (Ls : List (ℕ × Bool)) (R : List Sym), R.head?.bind Sym.bit? = none →
      ∀ (o : List Bool) (n : ℕ) (v : Bool),
      (Ls.flatMap Check.litRev).length + (ds.flatMap itemTok).length ≤ Lb →
      ∃ v', RunLe prog ((Ls.flatMap Check.litRev).length * (7 * Lb + 7))
        ⟨some .lits, v, st (Ls.reverse.flatMap Check.litRev ++ R) o [] (ds.flatMap itemTok) []
          c n⟩
        ⟨some .lits, v', st R (lrows ds Ls ++ o) [] ((Ls.map some ++ ds).flatMap itemTok) []
          c (n + Ls.length)⟩

Uses 15 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · Tokens of an item on the walked stack · Rows pushed for a clause's literals · The CLIQUE emitter machine · Configuration stacks of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · A literal's tokens on the token stack · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Runs within a step budget

Proof usesPolarity-first tokens of a literal · Emitter run over one literal occurrence · Bits pushed by a walk of the CLIQUE emitter · Exact-length runs of a TM2 machine

Used byClique emitter: one clause

TheoremClique emitter: one clause#✓fully proved

Let \(C\) be a clause, \(\varphi\) a CNF formula, \(R\) a token list that is empty or starts with a clause marker, \(o\) a list of bits, \(c, n, B \in \mathbb{N}\) and \(v\) a Boolean. Write \(T_C\) for the tokens of \(C\) as they lie on the token stack (a clause marker, then the literals last-first) and \(D_\psi\) for the tokens of the items of a formula \(\psi\). If \(|T_C| + |D_\varphi| \le B\), then for some flag \(v'\) the emitter machine goes in at most \(|T_C| \cdot (7B + 7)\) steps from label start with flag \(v\) and the state with token stack \(T_C\) followed by \(R\), output \(o\), walked stack \(D_\varphi\), clause count \(c\), occurrence count \(n\) and all other stacks empty, to label start with flag \(v'\) and the state with token stack \(R\), output the rows pushed for the literals of \(C\) walked above a clause marker and the items of \(\varphi\), followed by \(o\), walked stack \(D_{C \varphi}\) for the formula \(C\varphi\) with first clause \(C\), clause count \(c + 1\), occurrence count \(n + |C|\) and all other stacks empty.

theorem clause_run (Lb : ℕ) (C : CNFClause) (R : List Sym) (hR : R = [] ∨ R.head? = some .cl)
    (φ : CNF) (o : List Bool) (c n : ℕ) (v : Bool)
    (hb : (Check.clRev C).length + ((items φ).flatMap itemTok).length ≤ Lb) :
    ∃ v', RunLe prog ((Check.clRev C).length * (7 * Lb + 7))
      ⟨some .start, v, st (Check.clRev C ++ R) o [] ((items φ).flatMap itemTok) [] c n⟩
      ⟨some .start, v', st R (lrows (none :: items φ) C ++ o) []
        ((items (C :: φ)).flatMap itemTok) [] (c + 1) (n + C.length)⟩

Uses 19 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · Tokens of an item on the walked stack · Walked items of a formula · Rows pushed for a clause's literals · The CLIQUE emitter machine · Configuration stacks of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · A clause's tokens on the token stack · Stack alphabet of the SAT verifier · CNF formula · CNF clause · Runs within a step budget

Proof usesLiteral-marker test of the 3SAT emitter · Emitter run over a clause's literals · A literal's tokens on the token stack · Reading a symbol as a name bit · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byEmitter run over a formula's clauses

TheoremEmitter run over a formula's clauses#✓fully proved

Write \(\langle \ell, v \mid t, o, a, d, e, c, n\rangle\) for the configuration of the SAT-to-CLIQUE emitter at label \(\ell\) with local bit \(v\), stacks \(T = t\), \(O = o\), \(A = a\), \(D = d\), \(E = e\), empty scratch stacks \(B\) and \(X\), and \(c\) and \(n\) marks on the counters \(C\) and \(N\); juxtaposition of lists is concatenation. Let \(L \in \mathbb{N}\), let \(\varphi\) be a CNF formula with clauses \(C_1, \dots, C_m\) in order, let \(R\) be a list of symbols that is empty or starts with the clause marker, \(o\) a list of bits and \(v\) a bit. Let \(\kappa_i\) be the token list of \(C_i\) as it lies on the token stack and \(\tau = \kappa_m \cdots \kappa_1\). If \(|\tau| \le L\), then for some bit \(v'\) the machine goes in at most \(|\tau| (7L + 7)\) steps from \(\langle \mathsf{start}, v \mid \tau R, o, [], [], [], 0, 0\rangle\) to \(\langle \mathsf{start}, v' \mid R, \rho\, o, [], \delta, [], m, s\rangle\), where \(\rho\) is the row bits of \(\varphi\), \(\delta\) is the concatenation of the tokens of the items of \(\varphi\) and \(s = |C_1| + \dots + |C_m|\) is the total number of literals of \(\varphi\).

theorem formula_run (Lb : ℕ) :
    ∀ (φ : CNF) (R : List Sym), (R = [] ∨ R.head? = some .cl) → ∀ (o : List Bool) (v : Bool),
      (φ.reverse.flatMap Check.clRev).length ≤ Lb →
      ∃ v', RunLe prog ((φ.reverse.flatMap Check.clRev).length * (7 * Lb + 7))
        ⟨some .start, v, st (φ.reverse.flatMap Check.clRev ++ R) o [] [] [] 0 0⟩
        ⟨some .start, v', st R (rowsF φ ++ o) [] ((items φ).flatMap itemTok) [] φ.length
          φ.flatten.length⟩

Uses 19 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · Tokens of an item on the walked stack · Walked items of a formula · The CLIQUE emitter machine · Row bits of a formula for the CLIQUE emitter · Configuration stacks of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · A clause's tokens on the token stack · Stack alphabet of the SAT verifier · CNF formula · CNF clause · Runs within a step budget

Proof usesClique emitter: one clause · Polarity-first tokens of a literal · Reversing a list preserves the length of a flat map · Rows pushed for a clause's literals · A literal's tokens on the token stack · Exact-length runs of a TM2 machine

Used byThe CLIQUE emitter computes Karp's instance in cubic time

TheoremThe CLIQUE emitter computes Karp's instance in cubic time#✓fully proved

Let \(\varphi\) be a CNF formula with token list \(\tau\) (in reading order), \(o\) a list of Booleans, \(v\) a flag, and \(S\) stack contents in which the token stack \(T\) holds \(\tau\) reversed (stacks are listed top first), the output stack \(O\) holds \(o\) and every other stack is empty. Started at its start label with flag \(v\) and stacks \(S\), the CLIQUE emitter reaches the label \(\mathrm{done}\) in at most \(8(|\tau| + 1)^3\) steps, with some flag and stacks \(S'\) such that \(O\) holds, in \(S'\), Karp's CLIQUE instance of \(\varphi\) followed by \(o\).

theorem run (φ : CNF) (o : List Bool) (v : Bool) (St : ∀ k, List (Γ k))
    (hT : St .T = (toks φ).reverse) (hO : St .O = o) (h0 : ∀ k, k ≠ .T → k ≠ .O → St k = []) :
    ∃ v' S', RunLe prog (8 * ((toks φ).length + 1) ^ 3) ⟨some start, v, St⟩
      ⟨some .done, v', S'⟩ ∧ S' .O = toClique φ ++ o

Uses 29 · Used by 1

Statement usesStacks of the SAT-to-CLIQUE emitter · Labels of the SAT-to-CLIQUE emitter · The CLIQUE emitter machine · Start label of the CLIQUE emitter · Stack alphabets of the CLIQUE emitter · Karp's CLIQUE instance of a CNF formula · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · Runs within a step budget

Proof usesClique emitter: the instance prefix · Reversing a list preserves the length of a flat map · Emitter run over a formula's clauses · Tokens of an item on the walked stack · Walked items of a formula · Occurrences of a formula with a first clause · Row bits of a formula for the CLIQUE emitter · The CLIQUE emitter's row bits are Karp's pair bits · Configuration stacks of the CLIQUE emitter · Adjacency bits of Karp's clique graph · Encoding of a graph instance · Literal occurrences of a CNF formula · A clause's tokens on the token stack · A literal's tokens on the token stack · Tokens of a clause · Tokens of a literal · CNF clause · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byThe CLIQUE emitter

InductiveModes of the CLIQUE/VERTEX-COVER reduction machine#✓fully proved

A mode is one of two values, the flip mode and the vertex-cover mode. They select the reduction that the machine of this module computes: CLIQUE to INDEPENDENT-SET in the flip mode, INDEPENDENT-SET to VERTEX-COVER in the vertex-cover mode.

inductive Mode | flip | vc
  deriving DecidableEq

Used by 19

Used byReduction computed in each mode · Pair-bit transform of each mode · Counter of the first output number of the KG-map machine · CLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · The CLIQUE-to-INDEPENDENT-SET and INDEPENDENT-SET-to-VERTEX-COVER map as a host component · Moving the pair bits onto stack \(Y\) · Label after the move phase of the KG-map machine · Output phase of the KG-map machine · Output loop for the pair bits of the KG-map machine · The KG-map machine · Unterminated first unary number in the KG-map machine · Reading the first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Reading the second unary number in the KG-map machine · Correctness and running time of the KG-map machine · Failed subtraction in the KG-map machine · Subtraction loop of the clique reduction machine · Number output of the clique reduction machine

DefinitionReduction computed in each mode#✓fully proved

The map on bit strings that a mode of the CLIQUE/VERTEX-COVER reduction machine computes: in the flip mode it is the reduction from CLIQUE to INDEPENDENT-SET on bit strings, and in the vertex-cover mode it is the reduction from INDEPENDENT-SET to VERTEX-COVER on bit strings.

def Mode.f : Mode → List Bool → List Bool
  | .flip => flipKG
  | .vc => isToVc

Uses 3 · Used by 3

Statement usesModes of the CLIQUE/VERTEX-COVER reduction machine · Complementing map from CLIQUE to INDEPENDENT-SET instances · Map from INDEPENDENT-SET to VERTEX-COVER instances

Used byCLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · Correctness and running time of the KG-map machine

InductiveStacks of the CLIQUE to VERTEX-COVER reduction machine#✓fully proved

Stacks: input X, output O, counters A (k), B (n), D (n, then n - k), and the reversed pair bits Y.

inductive K | X | O | A | B | D | Y
  deriving DecidableEq

Used by 17

Used byStack alphabets of the clique reduction machine · Counter of the first output number of the KG-map machine · CLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · The CLIQUE-to-INDEPENDENT-SET and INDEPENDENT-SET-to-VERTEX-COVER map as a host component · Moving the pair bits onto stack \(Y\) · Output phase of the KG-map machine · Output loop for the pair bits of the KG-map machine · The KG-map machine · Unterminated first unary number in the KG-map machine · Reading the first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Reading the second unary number in the KG-map machine · Correctness and running time of the KG-map machine · Failed subtraction in the KG-map machine · Subtraction loop of the clique reduction machine · Number output of the clique reduction machine

DefinitionStack alphabets of the clique reduction machine#✓fully proved

The alphabet \(\Gamma(k)\) of a stack \(k\) is the Booleans if \(k\) is the output stack \(O\), and the token alphabet \(\mathrm{Sym}\) for every other stack (\(X\), \(A\), \(B\), \(D\) and \(Y\)).

@[reducible] def Γ : K → Type
  | .O => Bool
  | _ => Sym

Uses 2 · Used by 15

Statement usesStacks of the CLIQUE to VERTEX-COVER reduction machine · Stack alphabet of the SAT verifier

Used byCLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · The CLIQUE-to-INDEPENDENT-SET and INDEPENDENT-SET-to-VERTEX-COVER map as a host component · Moving the pair bits onto stack \(Y\) · Output phase of the KG-map machine · Output loop for the pair bits of the KG-map machine · The KG-map machine · Unterminated first unary number in the KG-map machine · Reading the first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Reading the second unary number in the KG-map machine · Correctness and running time of the KG-map machine · Failed subtraction in the KG-map machine · Subtraction loop of the clique reduction machine · Number output of the clique reduction machine

InductiveLabels of the KG-map machine#✓fully proved

The type of the ten instruction labels of the KG-map machine: read \(k\), read \(n\), move the pair bits, subtract, output the pair bits, output \(n\), write the separator, output the last number, the failure label and the halting label.

The machine reaches the subtraction label only in the vertex-cover mode, and at the failure label it writes the fixed no-instance.

inductive Lab | rdK | rdN | mv | sub | outY | outB | sep | outK | bad | done
  deriving DecidableEq

Used by 17

Used byCLIQUE ≤ INDEPENDENT-SET is polynomial-time · INDEPENDENT-SET ≤ VERTEX-COVER is polynomial-time · The CLIQUE-to-INDEPENDENT-SET and INDEPENDENT-SET-to-VERTEX-COVER map as a host component · Moving the pair bits onto stack \(Y\) · Label after the move phase of the KG-map machine · Output phase of the KG-map machine · Output loop for the pair bits of the KG-map machine · The KG-map machine · Unterminated first unary number in the KG-map machine · Reading the first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Reading the second unary number in the KG-map machine · Correctness and running time of the KG-map machine · Start label of the KG-map machine · Failed subtraction in the KG-map machine · Subtraction loop of the clique reduction machine · Number output of the clique reduction machine

AbbreviationCounter unit symbol of the clique reduction machine#✓fully proved

\(U\) is the symbol \(\mathsf{cl}\) of the token alphabet \(\mathrm{Sym}\).

It is the unit of the counter stacks \(A\), \(B\) and \(D\), which hold a number \(n\) as \(n\) copies of \(U\).

abbrev U : Sym := .cl

Uses 1 · Used by 10

Statement usesStack alphabet of the SAT verifier

Used byOutput phase of the KG-map machine · The KG-map machine · Unterminated first unary number in the KG-map machine · Reading the first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Reading the second unary number in the KG-map machine · Correctness and running time of the KG-map machine · Failed subtraction in the KG-map machine · Subtraction loop of the clique reduction machine · Number output of the clique reduction machine

DefinitionTest for the input bit true#✓fully proved

A test on the result of popping a stack: it is true exactly when a symbol was popped and that symbol is \(\mathrm{bit}(\mathrm{true})\), and false for every other symbol and for an empty stack.

def isT : Option Sym → Bool
  | some (.bit true) => true
  | _ => false

Uses 1 · Used by 6

Statement usesStack alphabet of the SAT verifier

Used byMoving the pair bits onto stack \(Y\) · The KG-map machine · Unterminated first unary number in the KG-map machine · Reading the first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Reading the second unary number in the KG-map machine

DefinitionTest for the moved bit true#✓fully proved

A test on the result of popping a stack: it is true exactly when a symbol was popped and that symbol is \(\mathrm{val}(\mathrm{true})\), and false for every other symbol and for an empty stack.

def isV : Option Sym → Bool
  | some (.val true) => true
  | _ => false

Uses 1 · Used by 2

Statement usesStack alphabet of the SAT verifier

Used byOutput loop for the pair bits of the KG-map machine · The KG-map machine

DefinitionPair-bit transform of each mode#✓fully proved

For a mode of the CLIQUE/VERTEX-COVER reduction machine, the map on booleans applied to each pair bit as it is written to the output: negation in the flip mode and the identity in the vertex-cover mode.

def Mode.fb : Mode → Bool → Bool
  | .flip => not
  | .vc => id

Uses 1 · Used by 4

Statement usesModes of the CLIQUE/VERTEX-COVER reduction machine

Used byOutput phase of the KG-map machine · Output loop for the pair bits of the KG-map machine · The KG-map machine · Correctness and running time of the KG-map machine

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.