Value of a bit list with a leading bit to Reading a pair bit or vertex mark

TheoremValue of a bit list with a leading bit#✓fully proved

Write \(\mathrm{val}(l)\) for the value of a bit list \(l\) read as a binary number least significant bit first, and for a bit \(b\) write \([b]\) for \(1\) if \(b\) is true and \(0\) if \(b\) is false. For every bit \(b\) and every bit list \(l\), the list with first entry \(b\) followed by \(l\) has value \([b] + 2 \cdot \mathrm{val}(l)\).

@[simp] theorem bitsVal_cons (b : Bool) (l : List Bool) :
    bitsVal (b :: l) = b.toNat + 2 * bitsVal l

Uses 1 · Used by 5

Statement usesValue of a little-endian bit list

Used byValue of a list of two-bit digits · A bit list without trailing false is the binary code of its value · Binary code of the value of a bit list · Subset-sum emitter: one vertex number · Run of the VERTEX-COVER to SUBSET-SUM machine

TheoremA bit list without trailing false is the binary code of its value#✓fully proved

For every bit list \(l\) whose last entry is not false (the empty list included), the binary code, least significant bit first, of the value of \(l\) read least significant bit first is \(l\) itself.

theorem encodeNat_bitsVal : ∀ l : List Bool, l.getLast? ≠ some false → encodeNat (bitsVal l) = l

Uses 3 · Used by 3

Statement usesValue of a little-endian bit list

Proof usesValue of a bit list with a leading bit · Binary encoding, least significant bit first

Used byBinary code of the value of a bit list · Subset-sum emitter: one vertex number · Run of the VERTEX-COVER to SUBSET-SUM machine

TheoremValue of a list of two-bit digits#✓fully proved

Write \(\mathrm{val}(l)\) for the value of a bit list \(l\) read as a binary number least significant bit first. Let \(f\) assign to each bit a list of exactly two bits. Then for every bit list \(b_0, b_1, \dots, b_{m-1}\), the concatenation \(f(b_0) f(b_1) \cdots f(b_{m-1})\) has value \(\sum_{q < m} 4^q \, \mathrm{val}(f(b_q))\).

theorem bitsVal_flatMap2 (f : Bool → List Bool) (hf : ∀ b, (f b).length = 2) :
    ∀ bs : List Bool, bitsVal (bs.flatMap f) =
      ((List.range bs.length).map fun q => 4 ^ q * bitsVal (f (bs.getD q false))).sum

Uses 2 · Used by 2

Statement usesValue of a little-endian bit list

Proof usesValue of a bit list with a leading bit

Used bySubset-sum emitter: one vertex number · Run of the VERTEX-COVER to SUBSET-SUM machine

TheoremBinary code of the value of a bit list#✓fully proved

Read a bit list \(l\) as a binary number, least significant bit first. The binary code of its value (least significant bit first, with no trailing false bits) is \(l\) with all of its trailing false bits removed.

theorem encodeNat_bitsVal_rev (l : List Bool) :
    encodeNat (bitsVal l) = (l.reverse.dropWhile (!·)).reverse

Uses 3 · Used by 3

Statement usesValue of a little-endian bit list

Proof usesValue of a bit list with a leading bit · A bit list without trailing false is the binary code of its value

Used byConverter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Run of the VERTEX-COVER to SUBSET-SUM machine

TheoremDelimiting a bit list that ends in true#✓fully proved

For every bit list \(u = (u_1, \dots, u_k)\), the self-delimiting form of \(u\) followed by the bit true is \((\mathrm{true}, u_1, \mathrm{true}, u_2, \dots, \mathrm{true}, u_k, \mathrm{true}, \mathrm{true}, \mathrm{false})\).

theorem delimit_append_true (u : List Bool) :
    delimit (u ++ [true]) = u.flatMap (fun b => [true, b]) ++ [true, true, false]

Uses 1 · Used by 1

Statement usesSelf-delimiting form of a bitstring

Used byRun of the target-output phase of the subset-sum emitter

DefinitionOutput block of a vertex-number digit#✓fully proved

For a bit \(t\), the block is the four-bit list \((\mathrm{true}, t, \mathrm{true}, \mathrm{false})\).

In the reduction from VERTEX-COVER to SUBSET-SUM, the self-delimiting code of a vertex number consists of one such block for each pair digit, followed by \((\mathrm{true}, \mathrm{true}, \mathrm{false})\).

def blk (t : Bool) : List Bool := [true, t, true, false]

Used by 3

Used bySubset-sum emitter: one row of the pair walk · Subset-sum emitter: one vertex number · Run of the subset-sum emitter's pair walk

DefinitionOutput block of an edge number#✓fully proved

For \(q \in \mathbb{N}\) and a bit \(b\): if \(b\) is true, the block is \(q\) copies of \((\mathrm{true}, \mathrm{false}, \mathrm{true}, \mathrm{false})\) followed by \((\mathrm{true}, \mathrm{true}, \mathrm{false})\); if \(b\) is false, it is the one-bit list \((\mathrm{false})\).

This is the self-delimiting binary code of \(4^q\) when \(b\) is true and of \(0\) when \(b\) is false.

def edgeEnc (q : ℕ) (b : Bool) : List Bool :=
  if b then rep [true, false, true, false] q ++ [true, true, false] else [false]

Uses 1 · Used by 3

Statement usesRepeated block

Used byOutput of all edge numbers · Edge-number phase (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine

DefinitionOutput of all edge numbers#✓fully proved

Write \(E(q, b)\) for the output block of the edge number of pair \(q\) with bit \(b\). For a bit list \((b_{m-1}, \dots, b_1, b_0)\), listing the bit of the last pair first, the output is the concatenation \(E(0, b_0) \, E(1, b_1) \cdots E(m-1, b_{m-1})\).

def edgeOut : List Bool → List Bool
  | [] => []
  | b :: ds => edgeOut ds ++ edgeEnc ds.length b

Uses 1 · Used by 2

Statement usesOutput block of an edge number

Used byEdge-number phase (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine

DefinitionThe pair walk over lists of marks#✓fully proved

For lists \(L\) and \(R\) of booleans, the pair walk \(W(L, R)\) is the list of pairs of booleans defined by recursion on \(L\). If \(L\) is empty, then \(W(L, R)\) is empty. If \(L\) has first entry \(a\) and remaining entries \(L'\), then \(W(L, R)\) consists of the pairs \((a, r)\) for the entries \(r\) of \(R\) in order, followed by \(W(L', R')\), where \(R'\) is the list \(R\) with \(a\) put in front.

def walkM : List Bool → List Bool → List (Bool × Bool)
  | [], _ => []
  | a :: L, R => R.map (a, ·) ++ walkM L (a :: R)

Used by 5

Used byThe pair walk lists the vertex pairs in reverse · Touch bits from the pair walk of a vertex · Subset-sum emitter: one vertex number · Run of the subset-sum emitter's pair walk · Run of the VERTEX-COVER to SUBSET-SUM machine

DefinitionTriangular numbers#✓fully proved

For a natural number \(n\), the triangular number \(T(n)\) is the sum \(0 + 1 + \cdots + (n - 1)\) of the natural numbers below \(n\). It is defined by recursion: \(T(0) = 0\) and \(T(i + 1) = T(i) + i\).

def tri : ℕ → ℕ
  | 0 => 0
  | i + 1 => tri i + i

Used by 2

Used byRun of the pair-counting loop of the subset-sum emitter · Run of the VERTEX-COVER to SUBSET-SUM machine

TheoremThe pair walk lists the vertex pairs in reverse#✓fully proved

Let \(f\) be a function from the natural numbers to the booleans, let \(n\) be a natural number, and let \(W\) be the pair walk. For every \(i \le n\), let \(L\) be the list \(f(i - 1), \dots, f(1), f(0)\) (empty when \(i = 0\)) and \(R\) the list \(f(i), f(i + 1), \dots, f(n - 1)\) (empty when \(i = n\)). Then \(W(L, R)\) is obtained as follows: list the pairs \((a, j)\) of natural numbers with \(a < i\) and \(a < j < n\), with \(a\) ascending and, for each \(a\), \(j\) descending; reverse this list; and replace each pair \((a, j)\) by \((f(a), f(j))\).

theorem walkM_pairs (f : ℕ → Bool) (n : ℕ) : ∀ i ≤ n,
    walkM ((List.range i).map f).reverse ((List.range' i (n - i)).map f) =
      ((List.range i).flatMap fun a =>
        ((List.range n).reverse.filter (a < ·)).map (a, ·)).reverse.map fun p => (f p.1, f p.2)

Uses 1 · Used by 3

Statement usesThe pair walk over lists of marks

Used byTouch bits from the pair walk of a vertex · Subset-sum emitter: one vertex number · Run of the VERTEX-COVER to SUBSET-SUM machine

DefinitionVertex marks for a vertex#✓fully proved

For natural numbers \(n\) and \(v\), the list of \(n\) bits whose entries, from first to last, record for \(i = n-1, n-2, \dots, 0\) whether \(i = v\).

def mkL (n v : ℕ) : List Bool := ((List.range n).map (· == v)).reverse

Used by 5

Used byTouch bits from the pair walk of a vertex · Subset-sum emitter: one vertex number · Run of the mark-return loop of the subset-sum emitter · Run of the vertex-number phase of the subset-sum emitter · Run of the VERTEX-COVER to SUBSET-SUM machine

TheoremTouch bits from the pair walk of a vertex#✓fully proved

Let \(n\) and \(v\) be natural numbers, let \(m\) be the number of vertex pairs in encoding order for \(n\), and let \(b\) be a list of \(m\) pair bits. Let \(L\) be the list of vertex marks for \(v\) among \(n\), let \((x_0, y_0), \dots, (x_{k-1}, y_{k-1})\) be the pair walk \(W(L, [\,])\), and let \(c_0, \dots, c_{m-1}\) be the list \(b\) reversed. Then the list of the entries \(c_l \wedge (y_l \vee x_l)\) for \(l = 0, \dots, \min(k, m) - 1\), reversed, is the list of the values at \(q = 0, 1, \dots, m - 1\) of the test whether pair \(q\) touches \(v\) under \(b\).

theorem walk_touches (n : ℕ) (bits : List Bool) (v : ℕ) (hb : bits.length = (pairs n).length) :
    (List.zipWith (fun p b => b && (p.2 || p.1)) (walkM (mkL n v) []) bits.reverse).reverse =
      (List.range (pairs n).length).map (touches n bits v)

Uses 5 · Used by 1

Statement usesVertex marks for a vertex · The pair walk over lists of marks · Vertex pairs in encoding order · Pairs touching a vertex

Proof usesThe pair walk lists the vertex pairs in reverse

Used bySubset-sum emitter: one vertex number

InductiveStacks of the SUBSET-SUM reduction machine#✓fully proved

The machine has fifteen stacks: the input \(X\) and the output \(O\); \(A\), which holds the cover size \(k\), and \(H\), used to halve it; \(N\), which holds the number \(n\) of vertices, and \(M\), the pair count; \(C\), which counts the pair bits; the scratch stacks \(S_1\) and \(S_2\); \(Y\) and \(Z\), which hold the pair bits; \(T\), which holds the target's bits; and \(L\), \(R\) and \(R_t\), which hold the vertex marks.

inductive K | X | O | A | H | N | M | C | S1 | S2 | Y | Z | T | L | R | Rt
  deriving DecidableEq

Used by 27

Used byUnary-to-binary converter as a host component · Emitter stack embedding in the unary-to-binary converter · Program of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Stack alphabets of the subset-sum emitter · Edge-number phase (SUBSET-SUM reduction machine) · One halving step of the binary conversion (SUBSET-SUM reduction machine) · Subset-sum emitter: moving the pair bits · Subset-sum emitter: one row of the pair walk · The subset-sum emitter machine · Subset-sum emitter: unterminated unary prefix at rdK · Subset-sum emitter: reading the unary k · Subset-sum emitter: unterminated unary prefix at rdN · Subset-sum emitter: reading the unary n · Subset-sum emitter: one vertex number · Subset-sum emitter: moving unmarked vertices back to L · Run of the mark-return loop of the subset-sum emitter · Run of the pair-counting loop of the subset-sum emitter · Run of the vertex-number phase of the subset-sum emitter · Run of the subset-sum emitter's pair walk · Binary conversion (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine · Run of the target-bit loop of the subset-sum emitter · Run of the target-output phase of the subset-sum emitter · The VERTEX-COVER to SUBSET-SUM machine as a host component · The VERTEX-COVER to SUBSET-SUM reduction is polynomial-time

DefinitionStack alphabets of the subset-sum emitter#✓fully proved

In the VERTEX-COVER to SUBSET-SUM machine the output stack \(\mathsf{O}\) holds Booleans, and every other stack holds token symbols.

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

Uses 2 · Used by 26

Statement usesStacks of the SUBSET-SUM reduction machine · Stack alphabet of the SAT verifier

Used byUnary-to-binary converter as a host component · Emitter stack embedding in the unary-to-binary converter · Program of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Edge-number phase (SUBSET-SUM reduction machine) · One halving step of the binary conversion (SUBSET-SUM reduction machine) · Subset-sum emitter: moving the pair bits · Subset-sum emitter: one row of the pair walk · The subset-sum emitter machine · Subset-sum emitter: unterminated unary prefix at rdK · Subset-sum emitter: reading the unary k · Subset-sum emitter: unterminated unary prefix at rdN · Subset-sum emitter: reading the unary n · Subset-sum emitter: one vertex number · Subset-sum emitter: moving unmarked vertices back to L · Run of the mark-return loop of the subset-sum emitter · Run of the pair-counting loop of the subset-sum emitter · Run of the vertex-number phase of the subset-sum emitter · Run of the subset-sum emitter's pair walk · Binary conversion (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine · Run of the target-bit loop of the subset-sum emitter · Run of the target-output phase of the subset-sum emitter · The VERTEX-COVER to SUBSET-SUM machine as a host component · The VERTEX-COVER to SUBSET-SUM reduction is polynomial-time

InductiveLabels of the subset-sum emitter#✓fully proved

The control labels of the subset-sum emitter machine are: \(\mathrm{rdK}\), \(\mathrm{rdN}\) and \(\mathrm{mv}\) (parsing the two unary numbers \(k\) and \(n\) that open the input, and moving the pair bits); \(\mathrm{tri}\), \(\mathrm{triC}\), \(\mathrm{triC2}\), \(\mathrm{cmp}\) and, for every ordering \(o\), the labels \(\mathrm{rc}(o)\) and \(\mathrm{rcB}(o)\) (counting the pairs and comparing that count with the number of pair bits); \(\mathrm{eg}\), \(\mathrm{egX}\), \(\mathrm{egR}\), \(\mathrm{egR2}\) and \(\mathrm{egY}\) (the edge numbers); \(\mathrm{vinit}\), \(\mathrm{vtx}\), \(\mathrm{pr}\), \(\mathrm{rend}\), \(\mathrm{rmv}\), \(\mathrm{vend}\), \(\mathrm{vchk}\) and \(\mathrm{rs}\) (the vertex numbers); \(\mathrm{hv}\), \(\mathrm{hv0}\), \(\mathrm{hv1}\) and \(\mathrm{hvB}\) (the binary digits of \(k\)); \(\mathrm{tem0}\), \(\mathrm{tsk}\) and \(\mathrm{tem}\) (writing the target); \(\mathrm{bad}\), which writes the fixed no-instance; and the halting label \(\mathrm{done}\).

inductive Lab
  | rdK | rdN | mv | tri | triC | triC2 | cmp | rc (o : Ordering) | rcB (o : Ordering)
  | eg | egX | egR | egR2 | egY | vinit | vtx | pr | rend | rmv | vend | vchk | rs
  | hv | hv0 | hv1 | hvB | tem0 | tsk | tem | bad | done
  deriving DecidableEq

Used by 30

Used byUnary-to-binary converter as a host component · Label map from the emitter halt to scratch cleanup · Control labels of the unary-to-binary converter · Label enumeration of the unary-to-binary converter · Program of the unary-to-binary converter · Converter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Branch after the count comparison (SUBSET-SUM reduction machine) · Edge-number phase (SUBSET-SUM reduction machine) · One halving step of the binary conversion (SUBSET-SUM reduction machine) · Subset-sum emitter: moving the pair bits · Subset-sum emitter: one row of the pair walk · The subset-sum emitter machine · Subset-sum emitter: unterminated unary prefix at rdK · Subset-sum emitter: reading the unary k · Subset-sum emitter: unterminated unary prefix at rdN · Subset-sum emitter: reading the unary n · Subset-sum emitter: one vertex number · Subset-sum emitter: moving unmarked vertices back to L · Run of the mark-return loop of the subset-sum emitter · Start label of the subset-sum emitter · Run of the pair-counting loop of the subset-sum emitter · Run of the vertex-number phase of the subset-sum emitter · Run of the subset-sum emitter's pair walk · Binary conversion (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine · Run of the target-bit loop of the subset-sum emitter · Run of the target-output phase of the subset-sum emitter · The VERTEX-COVER to SUBSET-SUM machine as a host component · The VERTEX-COVER to SUBSET-SUM reduction is polynomial-time

AbbreviationCounter unit of the subset-sum emitter#✓fully proved

The unit symbol of the counters of the VERTEX-COVER to SUBSET-SUM machine is the token symbol \(\mathrm{cl}\); a counter with value \(n\) holds exactly \(n\) copies of it.

abbrev U : Sym := .cl

Uses 1 · Used by 13

Statement usesStack alphabet of the SAT verifier

Used byConverter turns a unary count into a canonical binary frame · Converter turns a unary count into a raw canonical binary payload · Edge-number phase (SUBSET-SUM reduction machine) · One halving step of the binary conversion (SUBSET-SUM reduction machine) · Subset-sum emitter: moving the pair bits · The subset-sum emitter machine · Subset-sum emitter: unterminated unary prefix at rdK · Subset-sum emitter: reading the unary k · Subset-sum emitter: unterminated unary prefix at rdN · Subset-sum emitter: reading the unary n · Run of the pair-counting loop of the subset-sum emitter · Binary conversion (SUBSET-SUM reduction machine) · Run of the VERTEX-COVER to SUBSET-SUM machine

DefinitionTest for the input bit true (SUBSET-SUM reduction machine)#✓fully proved

On the result of a pop, which is either a symbol or nothing (when the stack was empty), the test returns true exactly when the result is the input-bit symbol \(\mathrm{bit}(\mathrm{true})\), and false otherwise.

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

Uses 1 · Used by 9

Statement usesStack alphabet of the SAT verifier

Used byTesting a popped input bit · Subset-sum emitter: moving the pair bits · The subset-sum emitter machine · Subset-sum emitter: unterminated unary prefix at rdK · Subset-sum emitter: reading the unary k · Subset-sum emitter: unterminated unary prefix at rdN · Subset-sum emitter: reading the unary n · Run of the target-bit loop of the subset-sum emitter · Run of the target-output phase of the subset-sum emitter

DefinitionTest for the value symbol true (SUBSET-SUM reduction machine)#✓fully proved

On the result of a pop, which is either a symbol or nothing (when the stack was empty), the test returns true exactly when the result is the value symbol \(\mathrm{val}(\mathrm{true})\), which this machine uses for a pair bit or vertex mark that is true, and false otherwise.

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

Uses 1 · Used by 8

Statement usesStack alphabet of the SAT verifier

Used byEdge-number phase (SUBSET-SUM reduction machine) · Testing a popped input bit · Subset-sum emitter: one row of the pair walk · The subset-sum emitter machine · Subset-sum emitter: moving unmarked vertices back to L · Run of the mark-return loop of the subset-sum emitter · Run of the vertex-number phase of the subset-sum emitter · Run of the subset-sum emitter's pair walk

DefinitionReading a pair bit or vertex mark#✓fully proved

The partial map from token symbols to bits that sends the symbol \(\mathrm{val}(b)\) to \(b\) and gives no value on every other symbol.

def valOf : Sym → Option Bool
  | .val b => some b
  | _ => none

Uses 1 · Used by 5

Statement usesStack alphabet of the SAT verifier

Used byTesting a popped input bit · The subset-sum emitter machine · Subset-sum emitter: one vertex number · Run of the subset-sum emitter's pair walk · Run of the VERTEX-COVER to SUBSET-SUM machine

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.