Binary conversion (SUBSET-SUM reduction machine) to Statements of the SUBSET-SUM verifier

TheoremBinary conversion (SUBSET-SUM reduction machine)#✓fully proved

Let \(k\) be a natural number, \(v\) a value of the machine's Boolean flag and \(S\) an assignment of contents to the stacks, and list the binary digits of \(k\) least significant first, without leading zeros (so there are none for \(k = 0\)). Suppose stack \(A\) holds \(k\) copies of the unit symbol and stack \(H\) is empty. Then, starting at label \(\mathrm{hv}\) with flag \(v\) and stacks \(S\), the machine reaches label \(\mathrm{tem0}\) in at most \(6k + 1\) steps, with some flag \(v'\) and stacks \(S'\) such that \(S'(T)\) is the reverse of the list of input-bit symbols \(\mathrm{bit}(b)\) for these binary digits \(b\) of \(k\), followed by \(S(T)\), and every stack other than \(A\), \(H\), \(T\) holds the same contents as in \(S\).

The machine thus pushes the binary digits of \(k\) onto \(T\) least significant first.

theorem hv_run (k : ℕ) : ∀ (v : Bool) (St : ∀ k, List (Γ k)), St .A = cnt U k → St .H = [] →
    ∃ v' S', RunLe prog (6 * k + 1) ⟨some .hv, v, St⟩ ⟨some .tem0, v', S'⟩ ∧
      S' .T = ((encodeNat k).map Sym.bit).reverse ++ St .T ∧
      ∀ j, j ≠ .A → j ≠ .H → j ≠ .T → S' j = St j

Uses 15 · Used by 3

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Counter unit of the subset-sum emitter · The subset-sum emitter machine · Stack alphabets of the subset-sum emitter · Stack alphabet of the SAT verifier · Runs within a step budget · Unary counter

Proof usesOne halving step of the binary conversion (SUBSET-SUM reduction machine) · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Adding units to target stacks · Running a counter transfer · Binary encoding, least significant bit first

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

TheoremRun of the target-bit loop of the subset-sum emitter#✓fully proved

Let \(l = (b_1, \dots, b_m)\) be a list of bits. Start the VERTEX-COVER to SUBSET-SUM machine at label \(\mathsf{tem}\) with any state bit and with stacks \(S\) in which stack \(\mathsf{T}\) holds exactly the bit symbols of \(b_1, \dots, b_m\), top first. Then after exactly \(m + 1\) steps the machine is at label \(\mathsf{done}\) with some state bit and stacks \(S'\) in which the output stack \(\mathsf{O}\) holds, top first, \(\mathrm{true}, b_m, \mathrm{true}, b_{m-1}, \dots, \mathrm{true}, b_1\) followed by the contents of \(\mathsf{O}\) in \(S\), and every stack other than \(\mathsf{T}\) and \(\mathsf{O}\) is as in \(S\). That is, each popped bit \(b\) is written as \(b\) and then \(\mathrm{true}\).

theorem tem_run : ∀ (l : List Bool) (v : Bool) (St : ∀ k, List (Γ k)), St .T = l.map Sym.bit →
    ∃ v' S', Run prog (l.length + 1) ⟨some .tem, v, St⟩ ⟨some .done, v', S'⟩ ∧
      S' .O = l.reverse.flatMap (fun b => [true, b]) ++ St .O ∧
      ∀ j, j ≠ .T → j ≠ .O → S' j = St j

Uses 9 · Used by 1

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · The subset-sum emitter machine · Stack alphabets of the subset-sum emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesTest for the input bit true (SUBSET-SUM reduction machine) · Testing a popped input bit · A single step executes the statement at the current label

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

TheoremRun of the target-output phase of the subset-sum emitter#✓fully proved

Let \(l\) be a list of bits, let \(l'\) be \(l\) with its leading \(\mathrm{false}\) bits removed, and let \(o\) be a list of bits. Start the VERTEX-COVER to SUBSET-SUM machine at label \(\mathsf{tsk}\) with any state bit and with stacks \(S\) in which stack \(\mathsf{T}\) holds exactly the bit symbols of \(l\), first bit on top, and the output stack \(\mathsf{O}\) holds \(\mathrm{false}\) followed by \(o\). Then after exactly \(|l| + 1\) steps the machine is at label \(\mathsf{done}\) with some state bit and stacks \(S'\) in which \(\mathsf{O}\) holds the self-delimiting encoding of the reverse of \(l'\) followed by \(o\), and every stack other than \(\mathsf{T}\) and \(\mathsf{O}\) is as in \(S\). Here the self-delimiting encoding of a list replaces each bit \(b\) by \(\mathrm{true}, b\) and appends \(\mathrm{false}\).

theorem tsk_run : ∀ (l : List Bool) (v : Bool) (St : ∀ k, List (Γ k)) (o : List Bool),
    St .T = l.map Sym.bit → St .O = false :: o →
    ∃ v' S', Run prog (l.length + 1) ⟨some .tsk, v, St⟩ ⟨some .done, v', S'⟩ ∧
      S' .O = delimit (l.dropWhile (!·)).reverse ++ o ∧ ∀ j, j ≠ .T → j ≠ .O → S' j = St j

Uses 12 · Used by 3

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · The subset-sum emitter machine · Stack alphabets of the subset-sum emitter · Stack alphabet of the SAT verifier · Self-delimiting form of a bitstring · Exact-length runs of a TM2 machine

Proof usesDelimiting a bit list that ends in true · Test for the input bit true (SUBSET-SUM reduction machine) · Testing a popped input bit · Run of the target-bit loop of the subset-sum emitter · A single step executes the statement at the current label

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

TheoremRun of the VERTEX-COVER to SUBSET-SUM machine#✓fully proved

Let \(x\) be a bit string. Start the VERTEX-COVER to SUBSET-SUM machine at its start label with any state bit and with stacks in which the input stack \(\mathsf{X}\) holds the bit symbols of \(x\), first bit on top, and every other stack is empty. Then within at most \(40(|x| + 1)^4\) steps the machine reaches the label \(\mathsf{done}\) with some state bit and stacks in which the output stack \(\mathsf{O}\) holds, top first, the image of \(x\) under the bit-string reduction from VERTEX-COVER to SUBSET-SUM.

theorem run (x : List Bool) (v : Bool) (St : ∀ k, List (Γ k))
    (hX : St .X = x.map Sym.bit) (h0 : ∀ k, k ≠ .X → St k = []) :
    ∃ v' S', RunLe prog (40 * (x.length + 1) ^ 4) ⟨some start, v, St⟩ ⟨some .done, v', S'⟩ ∧
      S' .O = reduceSS x

Uses 54 · Used by 1

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · The subset-sum emitter machine · Start label of the subset-sum emitter · Stack alphabets of the subset-sum emitter · Reduction from VERTEX-COVER to SUBSET-SUM · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesCounter unit of the subset-sum emitter · Value of a bit list with a leading bit · Value of a list of two-bit digits · Branch after the count comparison (SUBSET-SUM reduction machine) · Output block of an edge number · Output of all edge numbers · Edge-number phase (SUBSET-SUM reduction machine) · A bit list without trailing false is the binary code of its value · Binary code of the value of a bit list · Binary conversion (SUBSET-SUM reduction machine) · Testing a popped input bit · Vertex marks for a vertex · Subset-sum emitter: moving the pair bits · 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 · Triangular numbers · Run of the pair-counting loop of the subset-sum emitter · Run of the target-output phase of the subset-sum emitter · Reading a pair bit or vertex mark · Run of the vertex-number phase of the subset-sum emitter · The pair walk over lists of marks · The pair walk lists the vertex pairs in reverse · Edge numbers of the SUBSET-SUM reduction · Bit-string encoding of SUBSET-SUM instances · Fixed no-instance of SUBSET-SUM · Place value of a vertex pair in the SUBSET-SUM reduction · Vertex pairs in encoding order · Numbers of the SUBSET-SUM reduction · Target of the SUBSET-SUM reduction · Vertex numbers of the SUBSET-SUM reduction · Reading a unary length prefix · Self-delimiting form of a bitstring · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Non-destructive comparison of two counters · Unary counter · Pushing a constant list · Prepending a constant list · Running the bit-moving loop · Pushing a list of symbols onto one stack · Repeated block · Value of a little-endian bit list · Binary encoding, least significant bit first

Used byThe VERTEX-COVER to SUBSET-SUM reduction is polynomial-time

DefinitionWhether a bit string ends in false#✓fully proved

For a Boolean \(z\) and a list of bits \(p\), the value is \(z\) when \(p\) is empty and the negation of the last bit of \(p\) otherwise. So if \(z\) records whether the bits read so far end in false, the value records whether those bits followed by \(p\) end in false.

With \(z\) false the value is true exactly when \(p\) is non-empty and ends in false, that is, when \(p\) is not the canonical binary code of a number, least significant bit first.

def lastF : Bool → List Bool → Bool
  | z, [] => z
  | _, b :: p => lastF (!b) p

Used by 9

Used byDecoding a SUBSET-SUM instance inverts its encoding · Canonical binary strings are those not ending in zero · The verifier rejects a chosen block that ends in false · Adding a canonical chosen block · Skipping a number block · Reading the target block · The summing loop of the SUBSET-SUM verifier · The SUBSET-SUM verifier machine · SUBSET-SUM verifier computes the mask-selected sum

TheoremCanonical binary strings are those not ending in zero#✓fully proved

For every bit string \(p\), encoding in binary (least significant bit first) the natural number that \(p\) decodes to gives back \(p\) if and only if the trailing-zero test, started with no trailing zero, reports that \(p\) does not end in \(0\); that is, \(p\) is empty or its last bit is \(1\).

theorem encodeNat_decodeNat_iff (p : List Bool) :
    encodeNat (decodeNat p) = p ↔ lastF false p = false

Uses 2 · Used by 4

Statement usesWhether a bit string ends in false

Proof usesCanonical binary names

Used byDecoding a SUBSET-SUM instance inverts its encoding · The summing loop of the SUBSET-SUM verifier · The SUBSET-SUM verifier machine · SUBSET-SUM verifier computes the mask-selected sum

DefinitionParsing number blocks, with fuel#✓fully proved

For a fuel \(n\) and a list of bits \(r\), the result is either a list of numbers or a failure. If \(r\) is empty, the result is the empty list. If \(r\) is non-empty and \(n = 0\), parsing fails. If \(r\) is non-empty and \(n = m + 1\), one prefix-coded number is decoded off the front of \(r\): if this gives a number \(a\) with remainder \(r'\), the result is \(a\) followed by the result for \(r'\) with fuel \(m\) (failing if that fails), and otherwise parsing fails. Here the prefix code of \(a\) is the canonical binary code of \(a\), least significant bit first, with each bit \(b\) written as the pair true, \(b\), followed by a final false.

def numsAux : ℕ → List Bool → Option (List ℕ)
  | _, [] => some []
  | 0, _ :: _ => none
  | n + 1, b :: l => match decodeNatPrefix (b :: l) with
    | some (a, r) => (numsAux n r).map (a :: ·)
    | none => none

Uses 1 · Used by 5

Statement usesDecoding a prefix-coded natural number

Used byDecoding a SUBSET-SUM instance · Decoding a SUBSET-SUM instance inverts its encoding · The summing loop of the SUBSET-SUM verifier · The SUBSET-SUM verifier machine · SUBSET-SUM verifier computes the mask-selected sum

DefinitionDecoding a SUBSET-SUM instance#✓fully proved

A block holding a bit string \(p\) writes each bit \(b\) of \(p\) as the two bits \(1, b\) and ends with a single \(0\). The decoder reads a bit string \(x\) as one block holding the target \(t\), followed by blocks holding numbers \(a_1, \dots, a_n\) that run exactly to the end of \(x\), where each block must hold the canonical binary representation of its number (least significant bit first, no trailing \(0\)). It returns the list \((a_1, \dots, a_n)\) together with \(t\), and fails if \(x\) does not split this way.

def decodeSS (x : List Bool) : Option (List ℕ × ℕ) :=
  match decodeNatPrefix x with
  | some (t, r) => (numsAux r.length r).map fun as => (as, t)
  | none => none

Uses 2 · Used by 8

Statement usesParsing number blocks, with fuel · Decoding a prefix-coded natural number

Used byEncoded reduction from SUBSET-SUM to PARTITION · Correctness of the encoded SUBSET-SUM to PARTITION reduction · Encoded SUBSET-SUM to PARTITION map has linear output length · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Decoding a SUBSET-SUM instance inverts its encoding · The SUBSET-SUM verifier · SUBSET-SUM is characterized by its verifier · The SUBSET-SUM verifier machine

TheoremDecoding a SUBSET-SUM instance inverts its encoding#✓fully proved

For every bit string \(x\), every list \(a\) of natural numbers and every natural number \(t\), the SUBSET-SUM decoder returns the instance \((a, t)\) on \(x\) if and only if \(x\) is the encoding of the SUBSET-SUM instance with numbers \(a\) and target \(t\).

theorem decodeSS_eq_some {x : List Bool} {as : List ℕ} {t : ℕ} :
    decodeSS x = some (as, t) ↔ encodeSS as t = x

Uses 10 · Used by 4

Statement usesDecoding a SUBSET-SUM instance · Bit-string encoding of SUBSET-SUM instances

Proof usesCanonical binary strings are those not ending in zero · Whether a bit string ends in false · Parsing number blocks, with fuel · Decoding a prefix-coded natural number · Prefix-free code of a natural number · Parsing a self-delimiting block · Self-delimiting form of a bitstring · Parsing one self-delimiting block

Used byCorrectness of the encoded SUBSET-SUM to PARTITION reduction · Encoded SUBSET-SUM to PARTITION map has linear output length · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · SUBSET-SUM is characterized by its verifier

DefinitionNumbers chosen by a mask#✓fully proved

For a list of numbers \(a_0, \dots, a_{k-1}\) and a list of bits \(w\), the list of those \(a_i\) with \(w_i\) true, in their original order, where positions \(i\) beyond the end of \(w\) count as false.

def pick : List ℕ → List Bool → List ℕ
  | [], _ => []
  | a :: as, w => if w.headD false then a :: pick as w.tail else pick as w.tail

Used by 11

Used byQuadratic run of the padding machine on canonical instances · Canonical PARTITION membership transducer runs in quadratic time · Every sublist is selected by a mask · The SUBSET-SUM verifier · SUBSET-SUM is characterized by its verifier · The summing loop of the SUBSET-SUM verifier · A long enough all-true mask selects the whole list · The SUBSET-SUM verifier machine · Binary addition of framed numbers in quadratic time · SUBSET-SUM verifier computes the mask-selected sum · Embedded SUBSET-SUM summing component reaches the mapped label

DefinitionThe SUBSET-SUM verifier#✓fully proved

For bit strings \(x\) and \(w\), the verifier accepts \((x, w)\) exactly when \(x\) is the encoding of a SUBSET-SUM instance with numbers \(a_0, \dots, a_{n-1}\) and target \(t\), and the sum of the \(a_i\) for which bit \(i\) of \(w\) is true equals \(t\); bits beyond the end of \(w\) count as false, and bits of \(w\) past position \(n - 1\) are ignored. If \(x\) is not the encoding of an instance, the verifier rejects.

def ssCheck (x w : List Bool) : Bool :=
  match decodeSS x with
  | some (as, t) => (pick as w).sum == t
  | none => false

Uses 2 · Used by 3

Statement usesDecoding a SUBSET-SUM instance · Numbers chosen by a mask

Used bySUBSET-SUM is characterized by its verifier · The SUBSET-SUM verifier machine · SUBSET-SUM is in NP

TheoremEvery sublist is selected by a mask#✓fully proved

If \(l\) is a sublist of a list \(a\) of natural numbers, then there is a list \(w\) of Booleans of the same length as \(a\) such that the entries \(a_i\) of \(a\) with \(w_i\) true, taken in order, form exactly \(l\).

theorem exists_pick {l as : List ℕ} (h : l.Sublist as) :
    ∃ w : List Bool, w.length = as.length ∧ pick as w = l

Uses 1 · Used by 1

Statement usesNumbers chosen by a mask

Used bySUBSET-SUM is characterized by its verifier

TheoremSUBSET-SUM is characterized by its verifier#✓fully proved

A bit string \(x\) is a yes-instance of SUBSET-SUM if and only if there is a bit string \(w\) with \(|w| \le |x|\) such that the SUBSET-SUM verifier accepts \((x, w)\).

theorem subsetSumDec_iff (x : List Bool) :
    subsetSumDec x = true ↔ ∃ w, w.length ≤ x.length ∧ ssCheck x w = true

Uses 8 · Used by 1

Statement usesThe SUBSET-SUM verifier · The SUBSET-SUM problem

Proof usesDecoding a SUBSET-SUM instance · Decoding a SUBSET-SUM instance inverts its encoding · Every sublist is selected by a mask · Numbers chosen by a mask · Bit-string encoding of SUBSET-SUM instances · Self-delimiting form of a bitstring

Used bySUBSET-SUM is in NP

DefinitionCarry bit of a full adder#✓fully proved

For bits \(a\), \(b\) and a carry-in \(c\), the carry out of adding \(a\), \(b\) and \(c\) is \((a \wedge b) \vee (c \wedge (a \oplus b))\), which is true iff at least two of \(a\), \(b\), \(c\) are true.

def carry (a b c : Bool) : Bool := a && b || c && (a ^^ b)

Used by 12

Used byPadding reduction has linear output length · Bitlength of a PARTITION sum is at most the encoded length · PARTITION membership instance has linear bitlength · Ripple-carry addition of bit lists · Addition is correct on canonical numbers · The verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · Adding a canonical chosen block · Adding one payload bit to the sum · Bit length of the sum is at most the input length · The summing loop of the SUBSET-SUM verifier · Binary addition of framed numbers in quadratic time

DefinitionAdding a carry bit#✓fully proved

For a carry bit \(c\) and a bit string \(u\) (least significant bit first), \(\mathrm{inc}(c, u)\) adds \(c\) to \(u\) by ripple carry: on the empty string it is \([1]\) if \(c\) is true and empty otherwise, and on a string with first bit \(a\) and rest \(u'\) it is the bit \(a \oplus c\) followed by \(\mathrm{inc}(a \wedge c, u')\).

def incB : Bool → List Bool → List Bool
  | c, [] => if c then [true] else []
  | c, a :: u => (a ^^ c) :: incB (a && c) u

Used by 9

Used byPadding reduction has linear output length · Bitlength of a PARTITION sum is at most the encoded length · PARTITION membership instance has linear bitlength · Ripple-carry addition of bit lists · Addition is correct on canonical numbers · Adding a canonical chosen block · Carry phase of the SUBSET-SUM verifier · Bit length of the sum is at most the input length · The summing loop of the SUBSET-SUM verifier

DefinitionRipple-carry addition of bit lists#✓fully proved

For a carry-in bit \(c\) and bit lists \(u\) and \(p\), both least significant bit first, the ripple-carry sum walks \(p\). If \(p\) is empty, the result is \(u\) with the carry \(c\) added (a final carry becomes a new last bit). Otherwise, with \(a\) the first bit of \(u\) (\(a\) is false when \(u\) is empty) and \(b\) the first bit of \(p\), the result is the bit \(a \oplus b \oplus c\) followed by the ripple-carry sum of the rest of \(u\) and the rest of \(p\) with carry-in the carry out of \(a\), \(b\) and \(c\).

def addB : Bool → List Bool → List Bool → List Bool
  | c, u, [] => incB c u
  | c, u, b :: p =>
      (u.headD false ^^ b ^^ c) :: addB (carry (u.headD false) b c) u.tail p

Uses 2 · Used by 7

Statement usesCarry bit of a full adder · Adding a carry bit

Used byPadding reduction has linear output length · Bitlength of a PARTITION sum is at most the encoded length · PARTITION membership instance has linear bitlength · Addition is correct on canonical numbers · Adding a canonical chosen block · Bit length of the sum is at most the input length · The summing loop of the SUBSET-SUM verifier

TheoremAddition is correct on canonical numbers#✓fully proved

For every bit \(c\) and all natural numbers \(m\) and \(n\), the ripple-carry sum, with carry-in \(c\), of the canonical binary expansions of \(m\) and \(n\) (least significant bit first, no trailing false bit) is the canonical binary expansion of \(m + n + c\), where \(c\) counts as \(1\) if true and \(0\) if false. In particular the sum stays canonical.

theorem addB_encodeNat (c : Bool) (m n : ℕ) :
    addB c (encodeNat m) (encodeNat n) = encodeNat (m + n + c.toNat)

Uses 4 · Used by 5

Statement usesRipple-carry addition of bit lists

Proof usesCarry bit of a full adder · Adding a carry bit · Binary encoding, least significant bit first

Used byPadding reduction has linear output length · Bitlength of a PARTITION sum is at most the encoded length · PARTITION membership instance has linear bitlength · Bit length of the sum is at most the input length · The summing loop of the SUBSET-SUM verifier

InductiveStacks of the SUBSET-SUM verifier#✓fully proved

The verifier has seven stacks: the input \(X\), the witness \(W\), the target \(T\) (most significant bit on top), the running sum \(A\) (least significant bit on top), the new sum \(B\) (most significant bit on top), and the scratch stacks \(P\) and \(Q\) of the final comparison.

inductive K | X | W | T | A | B | P | Q
  deriving DecidableEq

Used by 51

Used byRaw-input SUBSET-SUM to PARTITION machine as a host component · SUBSET-SUM to PARTITION padding machine as a host component · Raw-input PARTITION membership machine as a host component · Canonical PARTITION membership transducer as a host component · Doubling-machine stack embedding in the membership transducer · Padding machine embeds the summation machine · Membership transducer embeds the summation machine · SUBSET-SUM to PARTITION map is polynomial-time · PARTITION to SUBSET-SUM map is polynomial-time · Stacks of the SUBSET-SUM to PARTITION padding machine · Stacks of the canonical PARTITION membership transducer · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the SUBSET-SUM to PARTITION padding machine · Program of the canonical PARTITION membership transducer · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Summation-machine stack embedding in the padding machine · Summation-machine stack embedding in the membership transducer · Stack alphabets of the canonical PARTITION membership transducer · Statements of the SUBSET-SUM verifier · The verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · Adding a canonical chosen block · Adding one payload bit to the sum · Moving the new sum back · Comparing the sum with the target · Carry phase of the SUBSET-SUM verifier · Carry step of the SUBSET-SUM verifier · Moving the final sum for the comparison · Starting the next number · The SUBSET-SUM verifier program · Reading one pair of a block · Rejection by the SUBSET-SUM verifier within a step bound · Rejecting in one step · The verifier rejects an unterminated skipped block · Skipping a number block · Stack contents of the SUBSET-SUM verifier · The verifier rejects an unterminated target block · Reading the target block · Identity embedding of the verifier stacks · The summing loop of the SUBSET-SUM verifier · Binary addition program built on the SUBSET-SUM machine · The SUBSET-SUM verifier machine · Binary addition of framed numbers in quadratic time · The SUBSET-SUM verifier machine as a host component · SUBSET-SUM is in NP · SUBSET-SUM verifier computes the mask-selected sum · Embedded SUBSET-SUM summing component reaches the mapped label · Embedded run of the binary addition component

InductiveLabels of the SUBSET-SUM verifier#✓fully proved

The verifier has the labels \(\mathrm{tgt}(z)\), reading the target; \(\mathrm{next}\), starting the next number; \(\mathrm{add}(c, z)\), adding a chosen number with carry \(c\); \(\mathrm{skip}(z)\), skipping an unchosen number; \(\mathrm{fin}(c)\), carrying \(c\) through the rest of the sum; \(\mathrm{back}\), moving the new sum back; \(\mathrm{fmove}\), moving the final sum for the comparison; \(\mathrm{cmp}\), comparing; \(\mathrm{yes}\), accepting; and \(\mathrm{no}\), rejecting, for all bits \(c\) and \(z\). In \(\mathrm{tgt}(z)\), \(\mathrm{add}(c, z)\) and \(\mathrm{skip}(z)\) the flag \(z\) records whether the bits of the current block read so far end in \(0\).

inductive Lab
  | tgt (z : Bool) | next | add (c z : Bool) | skip (z : Bool) | fin (c : Bool) | back | fmove
  | cmp | yes | no
  deriving DecidableEq

Used by 50

Used byRaw-input SUBSET-SUM to PARTITION machine as a host component · SUBSET-SUM to PARTITION padding machine as a host component · Raw-input PARTITION membership machine as a host component · Canonical PARTITION membership transducer as a host component · Padding machine embeds the summation machine · Membership transducer embeds the summation machine · Control labels of the SUBSET-SUM to PARTITION padding machine · Control labels of the canonical PARTITION membership transducer · Program of the raw-input SUBSET-SUM to PARTITION machine · Program of the SUBSET-SUM to PARTITION padding machine · Program of the raw-input PARTITION membership machine · Program of the canonical PARTITION membership transducer · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Quadratic run of the padding machine on canonical instances · Raw-input PARTITION membership machine runs in quadratic time · Canonical PARTITION membership transducer runs in quadratic time · Label map from summation halts to target emission · Label map from summation halts to the doubling pass · Statements of the SUBSET-SUM verifier · The verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · Adding a canonical chosen block · Adding one payload bit to the sum · Moving the new sum back · Comparing the sum with the target · Carry phase of the SUBSET-SUM verifier · Carry step of the SUBSET-SUM verifier · Moving the final sum for the comparison · Starting the next number · The SUBSET-SUM verifier program · Reading one pair of a block · Rejection by the SUBSET-SUM verifier within a step bound · Rejecting in one step · The verifier rejects an unterminated skipped block · Skipping a number block · Start state of the SUBSET-SUM verifier · The verifier rejects an unterminated target block · Reading the target block · Labels of the binary addition machine · The summing loop of the SUBSET-SUM verifier · Binary addition program built on the SUBSET-SUM machine · Redirection of the verifier's halt labels · Only halt labels are redirected to the cleanup label · The SUBSET-SUM verifier machine · Binary addition of framed numbers in quadratic time · The SUBSET-SUM verifier machine as a host component · SUBSET-SUM is in NP · SUBSET-SUM verifier computes the mask-selected sum · Embedded SUBSET-SUM summing component reaches the mapped label · Embedded run of the binary addition component

AbbreviationStatements of the SUBSET-SUM verifier#✓fully proved

The statements of the SUBSET-SUM verifier machine are the statements of a multi-stack Turing machine in Mathlib's TM2 model whose stacks are the seven stacks \(X\), \(W\), \(T\), \(A\), \(B\), \(P\), \(Q\), each over the symbol alphabet of the SAT verifier, whose labels are the labels of the SUBSET-SUM verifier, and whose local state is a Boolean.

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

Uses 3 · Used by 7

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

Used byThe verifier rejects an unterminated chosen block · The verifier rejects a chosen block that ends in false · Adding a canonical chosen block · Adding one payload bit to the sum · Carry step of the SUBSET-SUM verifier · Starting the next number · Reading one pair of a block

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.