Branch after the count comparison (SUBSET-SUM reduction machine) to One halving step of the binary conversion (SUBSET-SUM reduction machine)

DefinitionBranch after the count comparison (SUBSET-SUM reduction machine)#✓fully proved

The label the machine takes after comparing the pair-bit count with the pair count: the result "equal" leads to the label \(\mathrm{eg}\), which starts the edge-number phase, and the results "less than" and "greater than" lead to the failure label \(\mathrm{bad}\), which writes the fixed no-instance of SUBSET-SUM.

def cmpOut : Ordering → Lab
  | .eq => .eg
  | _ => .bad

Uses 1 · Used by 2

Statement usesLabels of the subset-sum emitter

Used byThe subset-sum emitter machine · Run of the VERTEX-COVER to SUBSET-SUM machine

DefinitionThe subset-sum emitter machine#✓fully proved

A multi-stack machine with the labels of the subset-sum emitter as control labels, a Boolean internal state, and the stacks of the emitter: the output stack \(O\) holds bits, every other stack holds symbols. Stacks are read top first, \(U\) is the counter unit, and to prepend a list to \(O\) is to push it so that it reads top first. The labels act as follows.

\(\mathrm{rdK}\): if \(X\) is empty, go to \(\mathrm{bad}\); otherwise pop \(X\), and if the popped symbol is \(\mathrm{bit}(\mathrm{true})\) push \(U\) on \(A\) and repeat, else go to \(\mathrm{rdN}\). \(\mathrm{rdN}\): the same, except that each \(\mathrm{bit}(\mathrm{true})\) pushes \(U\) on \(N\) and \(\mathrm{val}(\mathrm{false})\) on \(L\), and the other case goes to \(\mathrm{mv}\). \(\mathrm{mv}\): if \(X\) is empty, go to \(\mathrm{tri}\); otherwise pop \(X\), let \(s\) say whether the popped symbol is \(\mathrm{bit}(\mathrm{true})\), push \(\mathrm{val}(s)\) on \(Y\), then \(\mathrm{bit}(\mathrm{false})\) and \(\mathrm{bit}(s)\) on \(T\), then \(U\) on \(C\), and repeat.

\(\mathrm{tri}\): pop \(N\); if it was empty go to \(\mathrm{cmp}\), else go to \(\mathrm{triC}\), which pops \(N\) until it is empty, pushing \(U\) on \(M\) and on \(S_1\) for each popped symbol, and then to \(\mathrm{triC2}\), which pops \(S_1\) until it is empty, pushing \(U\) on \(N\) for each, and returns to \(\mathrm{tri}\). \(\mathrm{cmp}\): pop \(C\) and \(M\) together, pushing \(U\) on \(S_1\) for each symbol popped from \(C\) and on \(S_2\) for each symbol popped from \(M\), until one of them was empty; go to \(\mathrm{rc}(o)\) where \(o\) is \(<\), \(=\) or \(>\) according as only \(C\), both, or only \(M\) was empty. \(\mathrm{rc}(o)\) pops \(S_1\) until empty, pushing \(U\) on \(C\) for each, then \(\mathrm{rcB}(o)\) pops \(S_2\) until empty, pushing \(U\) on \(M\) for each, then goes to \(\mathrm{eg}\) if \(o\) is \(=\) and to \(\mathrm{bad}\) otherwise.

\(\mathrm{eg}\): if \(Y\) is empty, go to \(\mathrm{egY}\); otherwise pop \(Y\), let \(s\) say whether the popped symbol is \(\mathrm{val}(\mathrm{true})\), push \(\mathrm{val}(s)\) on \(Z\), pop \(C\) and \(M\), and if \(s\) is true prepend \((\mathrm{true}, \mathrm{true}, \mathrm{false})\) to \(O\) and go to \(\mathrm{egX}\), else prepend \((\mathrm{false})\) to \(O\) and repeat. \(\mathrm{egX}\) pops \(C\) until it is empty, prepending \((\mathrm{true}, \mathrm{false}, \mathrm{true}, \mathrm{false})\) to \(O\) for each popped symbol; then \(\mathrm{egR}\) pops \(M\) until empty, pushing \(U\) on \(C\) and on \(S_1\) for each, and \(\mathrm{egR2}\) pops \(S_1\) until empty, pushing \(U\) on \(M\) for each, and returns to \(\mathrm{eg}\). \(\mathrm{egY}\): while the top of \(Z\) is some \(\mathrm{val}(b)\), pop it and push \(\mathrm{val}(b)\) on \(Y\); then go to \(\mathrm{vinit}\).

\(\mathrm{vinit}\): pop \(L\); if a symbol was popped, push \(\mathrm{val}(\mathrm{true})\) on \(L\) and go to \(\mathrm{vtx}\), else go to \(\mathrm{hv}\). \(\mathrm{vtx}\): prepend \((\mathrm{true}, \mathrm{true}, \mathrm{false})\) to \(O\) and go to \(\mathrm{pr}\). \(\mathrm{pr}\): if \(R\) is empty, go to \(\mathrm{rend}\); otherwise pop \(R\), let \(m\) be true exactly when the popped symbol is \(\mathrm{val}(\mathrm{true})\) and push \(\mathrm{val}(m)\) on \(\mathrm{Rt}\), let \(a\) be true exactly when the top of \(L\) is \(\mathrm{val}(\mathrm{true})\), pop \(Y\), let \(b\) be true exactly when a \(\mathrm{val}(\mathrm{true})\) was popped and push \(\mathrm{val}(b)\) on \(Z\), prepend \((\mathrm{true}, b \wedge (m \vee a), \mathrm{true}, \mathrm{false})\) to \(O\), and repeat. \(\mathrm{rend}\): while the top of \(\mathrm{Rt}\) is some \(\mathrm{val}(b)\), pop it and push \(\mathrm{val}(b)\) on \(R\); then go to \(\mathrm{rmv}\). \(\mathrm{rmv}\): pop \(L\), push \(\mathrm{val}(t)\) on \(R\) where \(t\) is true exactly when a \(\mathrm{val}(\mathrm{true})\) was popped, and go to \(\mathrm{vend}\) if \(L\) is now empty, else to \(\mathrm{pr}\). \(\mathrm{vend}\): while the top of \(Z\) is some \(\mathrm{val}(b)\), pop it and push \(\mathrm{val}(b)\) on \(Y\); then go to \(\mathrm{vchk}\). \(\mathrm{vchk}\): go to \(\mathrm{hv}\) if the top of \(R\) is \(\mathrm{val}(\mathrm{true})\), else to \(\mathrm{rs}\). \(\mathrm{rs}\): if \(R\) is empty, go to \(\mathrm{vtx}\); otherwise pop \(R\); if the popped symbol is \(\mathrm{val}(\mathrm{true})\), pop \(L\) and push \(\mathrm{val}(\mathrm{true})\) and then \(\mathrm{val}(\mathrm{false})\) on \(L\), else push \(\mathrm{val}(\mathrm{false})\) on \(L\); repeat.

\(\mathrm{hv}\): go to \(\mathrm{tem0}\) if \(A\) is empty, else to \(\mathrm{hv0}\). \(\mathrm{hv0}\): pop \(A\); if it was empty, push \(\mathrm{bit}(\mathrm{false})\) on \(T\) and go to \(\mathrm{hvB}\), else go to \(\mathrm{hv1}\). \(\mathrm{hv1}\): pop \(A\); if it was empty, push \(\mathrm{bit}(\mathrm{true})\) on \(T\) and go to \(\mathrm{hvB}\), else push \(U\) on \(H\) and go to \(\mathrm{hv0}\). \(\mathrm{hvB}\) pops \(H\) until it is empty, pushing \(U\) on \(A\) for each, and returns to \(\mathrm{hv}\). \(\mathrm{tem0}\): prepend \((\mathrm{false})\) to \(O\) and go to \(\mathrm{tsk}\). \(\mathrm{tsk}\): if \(T\) is empty, go to \(\mathrm{done}\); otherwise pop \(T\), and if the popped symbol is \(\mathrm{bit}(\mathrm{true})\) prepend \((\mathrm{true}, \mathrm{true})\) to \(O\) and go to \(\mathrm{tem}\), else repeat. \(\mathrm{tem}\): if \(T\) is empty, go to \(\mathrm{done}\); otherwise pop \(T\), let \(s\) say whether the popped symbol is \(\mathrm{bit}(\mathrm{true})\), prepend \((\mathrm{true}, s)\) to \(O\), and repeat. \(\mathrm{bad}\): prepend the encoding of the subset-sum instance with no numbers and target \(1\) to \(O\) and go to \(\mathrm{done}\). \(\mathrm{done}\): halt.

Cslib.Complexity.Karp.EmitSS.prog · 69 lines

def prog : Lab → TM2.Stmt Γ Lab Bool
  | .rdK => .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .bad) <|
      .pop .X (fun _ o => isT o) <| .branch id
        (.push .A (fun _ => U) (.goto fun _ => .rdK)) (.goto fun _ => .rdN)
  | .rdN => .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .bad) <|
      .pop .X (fun _ o => isT o) <| .branch id
        (.push .N (fun _ => U) <| .push .L (fun _ => .val false) <| .goto fun _ => .rdN)
        (.goto fun _ => .mv)
  | .mv => .peek .X (fun _ o => o.isNone) <| .branch id (.goto fun _ => .tri) <|
      .pop .X (fun _ o => isT o) <| .push .Y (fun s => .val s) <|
      .push .T (fun _ => .bit false) <| .push .T (fun s => .bit s) <|
      .push .C (fun _ => U) <| .goto fun _ => .mv
  | .tri => decr .N .cmp .triC
  | .triC => xfer .N [⟨.M, U⟩, ⟨.S1, U⟩] .triC .triC2
  | .triC2 => xfer .S1 [⟨.N, U⟩] .triC2 .tri
  | .cmp => cmpStep .C .M .S1 .S2 U U .cmp (.rc .lt) (.rc .eq) (.rc .gt)
  | .rc o => xfer .S1 [⟨.C, U⟩] (.rc o) (.rcB o)
  | .rcB o => xfer .S2 [⟨.M, U⟩] (.rcB o) (cmpOut o)
  | .eg => .peek .Y (fun _ o => o.isNone) <| .branch id (.goto fun _ => .egY) <|
      .pop .Y (fun _ o => isV o) <| .push .Z (fun s => .val s) <|
      .pop .C (fun s _ => s) <| .pop .M (fun s _ => s) <| .branch id
        (.push .O (fun _ => false) <| .push .O (fun _ => true) <| .push .O (fun _ => true) <|
          .goto fun _ => .egX)
        (.push .O (fun _ => false) <| .goto fun _ => .eg)
  | .egX => xferE .C .O [true, false, true, false] .egX .egR
  | .egR => xfer .M [⟨.C, U⟩, ⟨.S1, U⟩] .egR .egR2
  | .egR2 => xfer .S1 [⟨.M, U⟩] .egR2 .eg
  | .egY => moveB .Z .Y valOf Sym.val .egY .vinit
  | .vinit => .pop .L (fun _ o => o.isSome) <| .branch id
      (.push .L (fun _ => .val true) <| .goto fun _ => .vtx) (.goto fun _ => .hv)
  | .vtx => emit .O [false, true, true] .pr
  | .pr => .peek .R (fun _ o => o.isNone) <| .branch id (.goto fun _ => .rend) <|
      .pop .R (fun _ o => isV o) <| .push .Rt (fun s => .val s) <|
      .peek .L (fun s o => s || isV o) <| .branch id
        (.pop .Y (fun _ o => isV o) <| .push .Z (fun s => .val s) <|
          .push .O (fun _ => false) <| .push .O (fun _ => true) <| .push .O (fun s => s) <|
          .push .O (fun _ => true) <| .goto fun _ => .pr)
        (.pop .Y (fun _ o => isV o) <| .push .Z (fun s => .val s) <|
          .push .O (fun _ => false) <| .push .O (fun _ => true) <| .push .O (fun _ => false) <|
          .push .O (fun _ => true) <| .goto fun _ => .pr)
  | .rend => moveB .Rt .R valOf Sym.val .rend .rmv
  | .rmv => .pop .L (fun _ o => isV o) <| .push .R (fun s => .val s) <|
      .peek .L (fun _ o => o.isNone) <| .branch id (.goto fun _ => .vend) (.goto fun _ => .pr)
  | .vend => moveB .Z .Y valOf Sym.val .vend .vchk
  | .vchk => .peek .R (fun _ o => isV o) <| .branch id (.goto fun _ => .hv)
      (.goto fun _ => .rs)
  | .rs => .peek .R (fun _ o => o.isNone) <| .branch id (.goto fun _ => .vtx) <|
      .pop .R (fun _ o => isV o) <| .branch id
        (.pop .L (fun s _ => s) <| .push .L (fun _ => .val true) <|
          .push .L (fun _ => .val false) <| .goto fun _ => .rs)
        (.push .L (fun _ => .val false) <| .goto fun _ => .rs)
  | .hv => .peek .A (fun _ o => o.isNone) <| .branch id (.goto fun _ => .tem0)
      (.goto fun _ => .hv0)
  | .hv0 => .pop .A (fun _ o => o.isSome) <| .branch id (.goto fun _ => .hv1)
      (.push .T (fun _ => .bit false) <| .goto fun _ => .hvB)
  | .hv1 => .pop .A (fun _ o => o.isSome) <| .branch id
      (.push .H (fun _ => U) <| .goto fun _ => .hv0)
      (.push .T (fun _ => .bit true) <| .goto fun _ => .hvB)
  | .hvB => xfer .H [⟨.A, U⟩] .hvB .hv
  | .tem0 => emit .O [false] .tsk
  | .tsk => .peek .T (fun _ o => o.isNone) <| .branch id (.goto fun _ => .done) <|
      .pop .T (fun _ o => isT o) <| .branch id
        (.push .O (fun _ => true) <| .push .O (fun _ => true) <| .goto fun _ => .tem)
        (.goto fun _ => .tsk)
  | .tem => .peek .T (fun _ o => o.isNone) <| .branch id (.goto fun _ => .done) <|
      .pop .T (fun _ o => isT o) <| .push .O (fun s => s) <| .push .O (fun _ => true) <|
      .goto fun _ => .tem
  | .bad => emitR .O noSS .done
  | .done => .halt

Uses 18 · Used by 23

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Counter unit of the subset-sum emitter · Branch after the count comparison (SUBSET-SUM reduction machine) · Test for the input bit true (SUBSET-SUM reduction machine) · Test for the value symbol true (SUBSET-SUM reduction machine) · Reading a pair bit or vertex mark · Stack alphabets of the subset-sum emitter · Fixed no-instance of SUBSET-SUM · Stack alphabet of the SAT verifier · Flag bit of a machine state · One round of counter comparison · Decrement · Pushing a constant list · Prepending a constant list · Bit-moving loop · Counter transfer loop · Draining a counter while prepending a block

Used byProgram 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 · 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

DefinitionStart label of the subset-sum emitter#✓fully proved

The VERTEX-COVER to SUBSET-SUM machine starts at the label \(\mathsf{rdK}\), which begins parsing the input by reading its leading unary number.

def start : Lab := .rdK

Uses 1 · Used by 2

Statement usesLabels of the subset-sum emitter

Used byRun of the VERTEX-COVER to SUBSET-SUM machine · The VERTEX-COVER to SUBSET-SUM reduction is polynomial-time

TheoremTesting a popped input bit#✓fully proved

For every bit \(b\), the test for the input bit true of the SUBSET-SUM reduction machine, applied to the popped symbol \(\mathrm{bit}(b)\), returns \(b\).

@[simp] theorem isT_bit (b : Bool) : isT (some (.bit b)) = b

Uses 2 · Used by 7

Statement usesTest for the input bit true (SUBSET-SUM reduction machine) · Stack alphabet of the SAT verifier

Used bySubset-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 · Run of the target-bit loop of the subset-sum emitter · Run of the target-output phase of the subset-sum emitter

TheoremTesting a popped input bit#✓fully proved

For every bit \(b\), the test for the input bit true of the SUBSET-SUM reduction machine, applied to the popped symbol \(\mathrm{bit}(b)\), returns \(b\).

@[simp] theorem isV_val (b : Bool) : isV (some (.val b)) = b

Uses 2 · Used by 6

Statement usesTest for the value symbol true (SUBSET-SUM reduction machine) · Stack alphabet of the SAT verifier

Used byEdge-number phase (SUBSET-SUM reduction machine) · Subset-sum emitter: one row of the pair walk · 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

TheoremTesting a popped input bit#✓fully proved

For every bit \(b\), the test for the input bit true of the SUBSET-SUM reduction machine, applied to the popped symbol \(\mathrm{bit}(b)\), returns \(b\).

theorem isBitBlock_val (l : List Bool) : IsBitBlock valOf (l.map Sym.val) l

Uses 3 · Used by 3

Statement usesReading a pair bit or vertex mark · Stack alphabet of the SAT verifier · Bit blocks

Used bySubset-sum emitter: one vertex number · Run of the subset-sum emitter's pair walk · Run of the VERTEX-COVER to SUBSET-SUM machine

TheoremSubset-sum emitter: reading the unary k#✓fully proved

Let \(k\) and \(i\) be natural numbers, \(v\) a Boolean state, \(r = (r_1, \dots, r_m)\) a list of bits and \(S\) stack contents such that stack \(X\) holds, top first, \(k\) copies of \(\mathrm{bit}(\mathrm{true})\), then \(\mathrm{bit}(\mathrm{false})\), then \(\mathrm{bit}(r_1), \dots, \mathrm{bit}(r_m)\), and stack \(A\) holds exactly \(i\) copies of the counter unit \(U\). Then \(k + 1\) steps of the subset-sum emitter machine lead from label \(\mathrm{rdK}\) with state \(v\) and stacks \(S\) to label \(\mathrm{rdN}\) with some state and some stacks \(S'\) such that \(S'(X)\) is \(\mathrm{bit}(r_1), \dots, \mathrm{bit}(r_m)\), \(S'(A)\) holds exactly \(i + k\) copies of \(U\), and every stack other than \(X\) and \(A\) is unchanged.

theorem rdK_some (k : ℕ) : ∀ (i : ℕ) (v : Bool) (St : ∀ k, List (Γ k)) (r : List Bool),
    St .X = (List.replicate k true ++ false :: r).map Sym.bit → St .A = cnt U i →
    ∃ v' S', Run prog (k + 1) ⟨some .rdK, v, St⟩ ⟨some .rdN, v', S'⟩ ∧
      S' .X = r.map Sym.bit ∧ S' .A = cnt U (i + k) ∧ ∀ j, j ≠ .X → j ≠ .A → S' j = St j

Uses 11 · Used by 1

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 · Exact-length runs of a TM2 machine · Unary counter

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 VERTEX-COVER to SUBSET-SUM machine

TheoremSubset-sum emitter: unterminated unary prefix at rdK#✓fully proved

Let \(r = (r_1, \dots, r_m)\) be a list of bits on which reading a unary length prefix fails (equivalently, no \(r_i\) is \(\mathrm{false}\)). Then for every Boolean state \(v\) and all stack contents \(S\) whose stack \(X\) holds \(\mathrm{bit}(r_1), \dots, \mathrm{bit}(r_m)\), top first, \(m + 1\) steps of the subset-sum emitter machine lead from label \(\mathrm{rdK}\) with state \(v\) and stacks \(S\) to label \(\mathrm{bad}\) with some state and some stacks that agree with \(S\) on every stack other than \(X\) and \(A\).

theorem rdK_none : ∀ (r : List Bool), readUnaryLength r = none →
    ∀ (v : Bool) (St : ∀ k, List (Γ k)), St .X = r.map Sym.bit →
      ∃ v' S', Run prog (r.length + 1) ⟨some .rdK, v, St⟩ ⟨some .bad, v', S'⟩ ∧
        ∀ j, j ≠ .X → j ≠ .A → S' j = St j

Uses 11 · 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 · Reading a unary length prefix · Exact-length runs of a TM2 machine

Proof usesCounter unit of the subset-sum emitter · Test 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 VERTEX-COVER to SUBSET-SUM machine

TheoremSubset-sum emitter: reading the unary n#✓fully proved

Let \(n\) and \(i\) be natural numbers, \(v\) a Boolean state, \(r = (r_1, \dots, r_m)\) a list of bits and \(S\) stack contents such that stack \(X\) holds, top first, \(n\) copies of \(\mathrm{bit}(\mathrm{true})\), then \(\mathrm{bit}(\mathrm{false})\), then \(\mathrm{bit}(r_1), \dots, \mathrm{bit}(r_m)\), stack \(N\) holds exactly \(i\) copies of the counter unit \(U\), and stack \(L\) holds exactly \(i\) copies of \(\mathrm{val}(\mathrm{false})\). Then \(n + 1\) steps of the subset-sum emitter machine lead from label \(\mathrm{rdN}\) with state \(v\) and stacks \(S\) to label \(\mathrm{mv}\) with some state and some stacks \(S'\) such that \(S'(X)\) is \(\mathrm{bit}(r_1), \dots, \mathrm{bit}(r_m)\), \(S'(N)\) holds exactly \(i + n\) copies of \(U\), \(S'(L)\) holds exactly \(i + n\) copies of \(\mathrm{val}(\mathrm{false})\), and every stack other than \(X\), \(N\) and \(L\) is unchanged.

theorem rdN_some (n : ℕ) : ∀ (i : ℕ) (v : Bool) (St : ∀ k, List (Γ k)) (r : List Bool),
    St .X = (List.replicate n true ++ false :: r).map Sym.bit → St .N = cnt U i →
    St .L = cnt (.val false) i →
    ∃ v' S', Run prog (n + 1) ⟨some .rdN, v, St⟩ ⟨some .mv, v', S'⟩ ∧
      S' .X = r.map Sym.bit ∧ S' .N = cnt U (i + n) ∧ S' .L = cnt (.val false) (i + n) ∧
      ∀ j, j ≠ .X → j ≠ .N → j ≠ .L → S' j = St j

Uses 11 · Used by 1

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 · Exact-length runs of a TM2 machine · Unary counter

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 VERTEX-COVER to SUBSET-SUM machine

TheoremSubset-sum emitter: unterminated unary prefix at rdN#✓fully proved

Let \(r = (r_1, \dots, r_m)\) be a list of bits on which reading a unary length prefix fails (equivalently, no \(r_i\) is \(\mathrm{false}\)). Then for every Boolean state \(v\) and all stack contents \(S\) whose stack \(X\) holds \(\mathrm{bit}(r_1), \dots, \mathrm{bit}(r_m)\), top first, \(m + 1\) steps of the subset-sum emitter machine lead from label \(\mathrm{rdN}\) with state \(v\) and stacks \(S\) to label \(\mathrm{bad}\) with some state and some stacks that agree with \(S\) on every stack other than \(X\), \(N\) and \(L\).

theorem rdN_none : ∀ (r : List Bool), readUnaryLength r = none →
    ∀ (v : Bool) (St : ∀ k, List (Γ k)), St .X = r.map Sym.bit →
      ∃ v' S', Run prog (r.length + 1) ⟨some .rdN, v, St⟩ ⟨some .bad, v', S'⟩ ∧
        ∀ j, j ≠ .X → j ≠ .N → j ≠ .L → S' j = St j

Uses 11 · 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 · Reading a unary length prefix · Exact-length runs of a TM2 machine

Proof usesCounter unit of the subset-sum emitter · Test 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 VERTEX-COVER to SUBSET-SUM machine

TheoremSubset-sum emitter: moving the pair bits#✓fully proved

Let \(r = (b_1, \dots, b_m)\) be a list of bits, \(v\) a Boolean state, \(c\) a natural number and \(S\) stack contents such that stack \(X\) holds \(\mathrm{bit}(b_1), \dots, \mathrm{bit}(b_m)\), top first, and stack \(C\) holds exactly \(c\) copies of the counter unit \(U\). Then \(m + 1\) steps of the subset-sum emitter machine lead from label \(\mathrm{mv}\) with state \(v\) and stacks \(S\) to label \(\mathrm{tri}\) with some state and some stacks \(S'\) such that: \(S'(Y)\) is \(S(Y)\) after pushing \(\mathrm{val}(b_1), \dots, \mathrm{val}(b_m)\) in turn; \(S'(T)\) is \(S(T)\) after pushing, for \(i = 1, \dots, m\) in turn, \(\mathrm{bit}(\mathrm{false})\) and then \(\mathrm{bit}(b_i)\); \(S'(C)\) holds exactly \(c + m\) copies of \(U\); and every stack other than \(X\), \(Y\), \(T\) and \(C\) is unchanged.

theorem mv_run (r : List Bool) : ∀ (v : Bool) (St : ∀ k, List (Γ k)) (c : ℕ),
    St .X = r.map Sym.bit → St .C = cnt U c →
    ∃ v' S', Run prog (r.length + 1) ⟨some .mv, v, St⟩ ⟨some .tri, v', S'⟩ ∧
      S' .Y = (r.map Sym.val).reverse ++ St .Y ∧
      S' .T = ((r.flatMap fun b => [false, b]).map Sym.bit).reverse ++ St .T ∧
      S' .C = cnt U (c + r.length) ∧ ∀ j, j ≠ .X → j ≠ .Y → j ≠ .T → j ≠ .C → S' j = St j

Uses 11 · Used by 1

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 · Exact-length runs of a TM2 machine · Unary counter

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 VERTEX-COVER to SUBSET-SUM machine

TheoremRun of the pair-counting loop of the subset-sum emitter#✓fully proved

Let \(n, p \in \mathbb{N}\) and let \(T_n = 0 + 1 + \dots + (n - 1)\). Start the VERTEX-COVER to SUBSET-SUM machine at label \(\mathsf{tri}\) with any state bit and with stacks \(S\) in which the counter stacks \(\mathsf{N}\) and \(\mathsf{M}\) hold exactly \(n\) and \(p\) unit symbols and the scratch stack \(\mathsf{S1}\) is empty. Then after exactly \((n + 1)^2\) steps the machine is at label \(\mathsf{cmp}\) with some state bit and stacks \(S'\) in which \(\mathsf{M}\) holds exactly \(p + T_n\) unit symbols and every stack other than \(\mathsf{N}\) and \(\mathsf{M}\) is as in \(S\).

theorem tri_run (n : ℕ) : ∀ (p : ℕ) (v : Bool) (St : ∀ k, List (Γ k)),
    St .N = cnt U n → St .M = cnt U p → St .S1 = [] →
    ∃ v' S', Run prog ((n + 1) ^ 2) ⟨some .tri, v, St⟩ ⟨some .cmp, v', S'⟩ ∧
      S' .M = cnt U (p + tri n) ∧ ∀ j, j ≠ .N → j ≠ .M → S' j = St j

Uses 13 · Used by 1

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 · Triangular numbers · Stack alphabets of the subset-sum emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Unary counter

Proof usesFlag bit of a machine state · A single step executes the statement at the current label · Copying a counter through a scratch stack · Decrement

Used byRun of the VERTEX-COVER to SUBSET-SUM machine

TheoremEdge-number phase (SUBSET-SUM reduction machine)#✓fully proved

Let \(d\) be a list of bits (in the machine, the pair bits listed from the last pair down), \(v\) a value of the machine's Boolean flag and \(S\) an assignment of contents to the stacks, and write \(\mathrm{val}(d)\) for the list of the symbols \(\mathrm{val}(b)\) for the entries \(b\) of \(d\), in order. Suppose stack \(Y\) holds \(\mathrm{val}(d)\) (first element on top), stacks \(C\) and \(M\) each hold \(|d|\) copies of the unit symbol, and stack \(S_1\) is empty. Then, starting at label \(\mathrm{eg}\) with flag \(v\) and stacks \(S\), the machine reaches label \(\mathrm{egY}\) in at most \(|d|(3|d| + 4) + 1\) steps, with some flag \(v'\) and stacks \(S'\) such that \(S'(Y)\) is empty, \(S'(Z)\) is the reverse of \(\mathrm{val}(d)\) followed by \(S(Z)\), \(S'(O)\) is the edge-number output of \(d\) followed by \(S(O)\), and every stack other than \(Y\), \(Z\), \(O\), \(C\), \(M\) holds the same contents as in \(S\).

For each pair \(q\) the machine pops its bit onto \(Z\) and writes its edge number, using \(C = M = q\).

theorem eg_run : ∀ (ds : List Bool) (v : Bool) (St : ∀ k, List (Γ k)),
    St .Y = ds.map Sym.val → St .C = cnt U ds.length → St .M = cnt U ds.length → St .S1 = [] →
    ∃ v' S', RunLe prog (ds.length * (3 * ds.length + 4) + 1) ⟨some .eg, v, St⟩
        ⟨some .egY, v', S'⟩ ∧
      S' .Y = [] ∧ S' .Z = (ds.map Sym.val).reverse ++ St .Z ∧ S' .O = edgeOut ds ++ St .O ∧
      ∀ j, j ≠ .Y → j ≠ .Z → j ≠ .O → j ≠ .C → j ≠ .M → S' j = St j

Uses 19 · Used by 1

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Counter unit of the subset-sum emitter · Output of all edge numbers · 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 usesOutput block of an edge number · Test for the value symbol true (SUBSET-SUM reduction machine) · Testing a popped input bit · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Copying a counter through a scratch stack · Pushing a list of symbols onto one stack · Repeated block · Draining a counter while prepending a block

Used byRun of the VERTEX-COVER to SUBSET-SUM machine

TheoremSubset-sum emitter: one row of the pair walk#✓fully proved

Stacks are listed top first. Let \(a\) be a bit, \(\ell\) a list of symbols, \((m_1, \dots, m_p)\) and \((b_1, \dots, b_p)\) two lists of bits of the same length \(p\), \(y\) a list of symbols, \(v\) a Boolean state and \(S\) stack contents such that \(S(R)\) is \(\mathrm{val}(m_1), \dots, \mathrm{val}(m_p)\), \(S(L)\) is \(\mathrm{val}(a)\) followed by \(\ell\), and \(S(Y)\) is \(\mathrm{val}(b_1), \dots, \mathrm{val}(b_p)\) followed by \(y\). For a bit \(t\) let \(\mathrm{blk}(t)\) be the list \((\mathrm{true}, t, \mathrm{true}, \mathrm{false})\), and put \(d_i = b_i \wedge (m_i \vee a)\). Then \(p + 1\) steps of the subset-sum emitter machine lead from label \(\mathrm{pr}\) with state \(v\) and stacks \(S\) to label \(\mathrm{rend}\) with some state and some stacks \(S'\) such that: \(S'(R)\) is empty; \(S'(\mathrm{Rt})\) is \(\mathrm{val}(m_p), \dots, \mathrm{val}(m_1)\) followed by \(S(\mathrm{Rt})\); \(S'(Y) = y\); \(S'(Z)\) is \(\mathrm{val}(b_p), \dots, \mathrm{val}(b_1)\) followed by \(S(Z)\); \(S'(O)\) is the concatenation \(\mathrm{blk}(d_p) \cdots \mathrm{blk}(d_1)\) followed by \(S(O)\); and every stack other than \(R\), \(\mathrm{Rt}\), \(Y\), \(Z\) and \(O\) is unchanged.

theorem pr_run (a : Bool) (l : List Sym) : ∀ (rs bs : List Bool) (v : Bool)
    (St : ∀ k, List (Γ k)) (yr : List Sym), rs.length = bs.length →
    St .R = rs.map Sym.val → St .L = .val a :: l → St .Y = bs.map Sym.val ++ yr →
    ∃ v' S', Run prog (rs.length + 1) ⟨some .pr, v, St⟩ ⟨some .rend, v', S'⟩ ∧
      S' .R = [] ∧ S' .Rt = (rs.map Sym.val).reverse ++ St .Rt ∧ S' .Y = yr ∧
      S' .Z = (bs.map Sym.val).reverse ++ St .Z ∧
      S' .O = (List.zipWith (fun mj b => b && (mj || a)) rs bs).reverse.flatMap blk ++ St .O ∧
      ∀ j, j ≠ .R → j ≠ .Rt → j ≠ .Y → j ≠ .Z → j ≠ .O → S' j = St j

Uses 10 · Used by 1

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Output block of a vertex-number digit · 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 value symbol true (SUBSET-SUM reduction machine) · Testing a popped input bit · A single step executes the statement at the current label

Used byRun of the subset-sum emitter's pair walk

TheoremRun of the subset-sum emitter's pair walk#✓fully proved

Let \(L_m \ne []\), \(r_m\) and \(w\) be lists of booleans, and for a list \(\ell\) of booleans write \(\bar\ell\) for the list of mark symbols \(\mathrm{val}(x)\), \(x \in \ell\). Let \((a_1, c_1), \dots, (a_m, c_m)\) be the mark pairs \(\mathrm{walkM}(L_m, r_m)\), and suppose \(w = (b_1, \dots, b_m)\) has the same length \(m\). Start the emitter machine at label \(\mathrm{pr}\) with any internal state \(v\) and stacks \(S\) such that \(S_L = \bar L_m\), \(S_R = \bar r_m\), \(S_{Rt}\) is empty and \(S_Y = \bar w \mathbin{+\!\!+} y\) for a list of symbols \(y\). Then after exactly \(2m + 3|L_m|\) steps the machine is at label \(\mathrm{vend}\), with some internal state \(v'\) and stacks \(S'\) such that \(S'_L\) and \(S'_{Rt}\) are empty, \(S'_R = \overline{\mathrm{rev}(L_m) \mathbin{+\!\!+} r_m}\), \(S'_Y = y\), \(S'_Z = \mathrm{rev}(\bar w) \mathbin{+\!\!+} S_Z\) and \(S'_O = \mathrm{blk}(t_m) \mathbin{+\!\!+} \cdots \mathbin{+\!\!+} \mathrm{blk}(t_1) \mathbin{+\!\!+} S_O\), where \(t_i = b_i \wedge (c_i \vee a_i)\) and \(\mathrm{blk}(t) = [\mathrm{true}, t, \mathrm{true}, \mathrm{false}]\); every stack other than \(L\), \(R\), \(Rt\), \(Y\), \(Z\) and \(O\) is unchanged.

The rows of the walk come from the vertex marks on \(L\) (top first) and the columns from the marks on \(R\); after each row the column marks are restored from \(Rt\) and the row mark moves onto \(R\).

theorem walk_run : ∀ (Lm rm wb : List Bool) (v : Bool) (St : ∀ k, List (Γ k)) (yr : List Sym),
    Lm ≠ [] → wb.length = (walkM Lm rm).length → St .L = Lm.map Sym.val →
    St .R = rm.map Sym.val → St .Rt = [] → St .Y = wb.map Sym.val ++ yr →
    ∃ v' S', Run prog (2 * wb.length + 3 * Lm.length) ⟨some .pr, v, St⟩ ⟨some .vend, v', S'⟩ ∧
      S' .L = [] ∧ S' .R = (Lm.reverse ++ rm).map Sym.val ∧ S' .Rt = [] ∧ S' .Y = yr ∧
      S' .Z = (wb.map Sym.val).reverse ++ St .Z ∧
      S' .O = (List.zipWith (fun p b => b && (p.2 || p.1)) (walkM Lm rm) wb).reverse.flatMap blk ++
        St .O ∧
      ∀ j, j ≠ .L → j ≠ .R → j ≠ .Rt → j ≠ .Y → j ≠ .Z → j ≠ .O → S' j = St j

Uses 17 · Used by 1

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Output block of a vertex-number digit · The subset-sum emitter machine · The pair walk over lists of marks · Stack alphabets of the subset-sum emitter · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesTesting a popped input bit · Test for the value symbol true (SUBSET-SUM reduction machine) · Testing a popped input bit · Subset-sum emitter: one row of the pair walk · Reading a pair bit or vertex mark · Flag bit of a machine state · Bit blocks · A single step executes the statement at the current label · Running the bit-moving loop

Used bySubset-sum emitter: one vertex number

TheoremSubset-sum emitter: one vertex number#✓fully proved

Stacks are listed top first. Let \(n\) be a natural number, \(p_0, \dots, p_{P-1}\) the pairs \((i, j)\) with \(i < j < n\) in encoding order (rows \(i\) ascending, within a row \(j\) descending), \((\beta_0, \dots, \beta_{P-1})\) a list of \(P\) pair bits and \(w < n\) a vertex. Let \(N_w = 4^P + \sum_q 4^q\), the sum over the \(q < P\) such that \(\beta_q\) is true and \(w\) is an endpoint of \(p_q\), and let \(m_u\) be true if \(u = w\) and false otherwise. Let \(v\) be a Boolean state and \(S\) stack contents such that \(S(L)\) is \(\mathrm{val}(m_{n-1}), \dots, \mathrm{val}(m_0)\), \(S(Y)\) is \(\mathrm{val}(\beta_{P-1}), \dots, \mathrm{val}(\beta_0)\), and \(S(R)\), \(S(\mathrm{Rt})\) and \(S(Z)\) are empty. Then \(3P + 3n + 2\) steps of the subset-sum emitter machine lead from label \(\mathrm{vtx}\) with state \(v\) and stacks \(S\) to label \(\mathrm{vchk}\) with some state and some stacks \(S'\) such that: \(S'(L)\), \(S'(\mathrm{Rt})\) and \(S'(Z)\) are empty; \(S'(R)\) is \(\mathrm{val}(m_0), \dots, \mathrm{val}(m_{n-1})\); \(S'(Y) = S(Y)\); \(S'(O)\) is the self-delimiting encoding of the binary representation of \(N_w\) (least significant bit first) followed by \(S(O)\); and every stack other than \(L\), \(R\), \(\mathrm{Rt}\), \(Y\), \(Z\) and \(O\) is unchanged.

theorem round_run (n : ℕ) (bits : List Bool) (hb : bits.length = (pairs n).length) (w : ℕ)
    (hw : w < n) (v : Bool) (St : ∀ k, List (Γ k)) (hL : St .L = (mkL n w).map Sym.val)
    (hR : St .R = []) (hRt : St .Rt = []) (hY : St .Y = bits.reverse.map Sym.val)
    (hZ : St .Z = []) :
    ∃ v' S', Run prog (3 * (pairs n).length + 3 * n + 2) ⟨some .vtx, v, St⟩
        ⟨some .vchk, v', S'⟩ ∧
      S' .L = [] ∧ S' .R = ((List.range n).map (· == w)).map Sym.val ∧ S' .Rt = [] ∧
      S' .Y = bits.reverse.map Sym.val ∧ S' .Z = [] ∧
      S' .O = delimit (encodeNat (vtxNum n bits w)) ++ St .O ∧
      ∀ j, j ≠ .L → j ≠ .R → j ≠ .Rt → j ≠ .Y → j ≠ .Z → j ≠ .O → S' j = St j

Uses 28 · Used by 1

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Vertex marks for a vertex · The subset-sum emitter machine · Stack alphabets of the subset-sum emitter · Vertex pairs in encoding order · Vertex numbers of the SUBSET-SUM reduction · Stack alphabet of the SAT verifier · Self-delimiting form of a bitstring · Exact-length runs of a TM2 machine

Proof usesValue of a bit list with a leading bit · Value of a list of two-bit digits · Output block of a vertex-number digit · A bit list without trailing false is the binary code of its value · Testing a popped input bit · Reading a pair bit or vertex mark · The pair walk over lists of marks · The pair walk lists the vertex pairs in reverse · Run of the subset-sum emitter's pair walk · Touch bits from the pair walk of a vertex · Place value of a vertex pair in the SUBSET-SUM reduction · Pairs touching a vertex · Flag bit of a machine state · A single step executes the statement at the current label · Pushing a constant list · Running the bit-moving loop · Pushing a list of symbols onto one stack · Value of a little-endian bit list

Used byRun of the vertex-number phase of the subset-sum emitter

TheoremSubset-sum emitter: moving unmarked vertices back to L#✓fully proved

Let \(c\) be a natural number, \(\rho = (\rho_1, \dots, \rho_k)\) a list of bits, \(v\) a Boolean state and \(S\) stack contents whose stack \(R\) holds, top first, \(c\) copies of \(\mathrm{val}(\mathrm{false})\) followed by \(\mathrm{val}(\rho_1), \dots, \mathrm{val}(\rho_k)\). Then \(c\) steps of the subset-sum emitter machine lead from label \(\mathrm{rs}\) with state \(v\) and stacks \(S\) back to label \(\mathrm{rs}\) with some state and some stacks \(S'\) such that \(S'(R)\) is \(\mathrm{val}(\rho_1), \dots, \mathrm{val}(\rho_k)\), \(S'(L)\) is \(c\) copies of \(\mathrm{val}(\mathrm{false})\) followed by \(S(L)\), and every stack other than \(R\) and \(L\) is unchanged.

theorem rsF_run (c : ℕ) : ∀ (v : Bool) (St : ∀ k, List (Γ k)) (rest : List Bool),
    St .R = (List.replicate c false ++ rest).map Sym.val →
    ∃ v' S', Run prog c ⟨some .rs, v, St⟩ ⟨some .rs, v', S'⟩ ∧ S' .R = rest.map Sym.val ∧
      S' .L = cnt (.val false) c ++ St .L ∧ ∀ j, j ≠ .R → j ≠ .L → S' j = St j

Uses 10 · 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 · Unary counter

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

Used byRun of the mark-return loop of the subset-sum emitter

TheoremRun of the mark-return loop of the subset-sum emitter#✓fully proved

Let \(n, w \in \mathbb{N}\) with \(w + 1 < n\). Start the VERTEX-COVER to SUBSET-SUM machine at label \(\mathsf{rs}\) with any state bit and with stacks \(S\) in which stack \(\mathsf{L}\) is empty and stack \(\mathsf{R}\) holds, top first, the symbols \(\mathrm{val}(b_0), \dots, \mathrm{val}(b_{n-1})\), where \(b_i\) is true exactly when \(i = w + 1\). Then after exactly \(n + 1\) steps the machine is at label \(\mathsf{vtx}\) with some state bit and stacks \(S'\) in which \(\mathsf{R}\) is empty, \(\mathsf{L}\) holds, top first, the symbols \(\mathrm{val}(c_{n-1}), \dots, \mathrm{val}(c_0)\), where \(c_i\) is true exactly when \(i = w\), and every stack other than \(\mathsf{R}\) and \(\mathsf{L}\) is as in \(S\). So the vertex mark moves from vertex \(w + 1\) to vertex \(w\).

theorem rs_run (n w : ℕ) (hw : w + 1 < n) (v : Bool) (St : ∀ k, List (Γ k))
    (hR : St .R = ((List.range n).map (· == w + 1)).map Sym.val) (hL : St .L = []) :
    ∃ v' S', Run prog (n + 1) ⟨some .rs, v, St⟩ ⟨some .vtx, v', S'⟩ ∧
      S' .L = (mkL n w).map Sym.val ∧ S' .R = [] ∧ ∀ j, j ≠ .R → j ≠ .L → S' j = St j

Uses 12 · Used by 1

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Vertex marks for a vertex · 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 value symbol true (SUBSET-SUM reduction machine) · Testing a popped input bit · Subset-sum emitter: moving unmarked vertices back to L · A single step executes the statement at the current label · Unary counter

Used byRun of the vertex-number phase of the subset-sum emitter

TheoremRun of the vertex-number phase of the subset-sum emitter#✓fully proved

Let \(n \in \mathbb{N}\), let \(p_0, \dots, p_{P-1}\) be the vertex pairs \((i, j)\) with \(i < j < n\), listed with \(i\) ascending and, for each \(i\), with \(j\) descending, let \(\beta_0, \dots, \beta_{P-1}\) be bits, and let \(w < n\). For a vertex \(u\) let \(a_u\) be \(4^P\) plus the sum of \(4^q\) over the indices \(q < P\) such that \(\beta_q\) is true and \(p_q\) contains \(u\). Start the VERTEX-COVER to SUBSET-SUM machine at label \(\mathsf{vtx}\) with any state bit and with stacks \(S\) in which stack \(\mathsf{L}\) holds, top first, the symbols \(\mathrm{val}(c_{n-1}), \dots, \mathrm{val}(c_0)\), where \(c_i\) is true exactly when \(i = w\), the stacks \(\mathsf{R}\), \(\mathsf{Rt}\) and \(\mathsf{Z}\) are empty, and stack \(\mathsf{Y}\) holds, top first, the symbols \(\mathrm{val}(\beta_{P-1}), \dots, \mathrm{val}(\beta_0)\). Then within at most \((w + 1)(3P + 4n + 4)\) steps the machine reaches label \(\mathsf{hv}\) with some state bit and stacks \(S'\) in which the output stack \(\mathsf{O}\) holds, top first, the self-delimiting binary encodings of \(a_0, a_1, \dots, a_w\) followed by the contents of \(\mathsf{O}\) in \(S\), and every stack other than \(\mathsf{L}\), \(\mathsf{R}\), \(\mathsf{Rt}\), \(\mathsf{Y}\), \(\mathsf{Z}\) and \(\mathsf{O}\) is as in \(S\). Here the binary encoding lists the bits least significant first, and the self-delimiting encoding replaces each bit \(b\) by \(\mathrm{true}, b\) and appends \(\mathrm{false}\).

theorem vtx_run (n : ℕ) (bits : List Bool) (hb : bits.length = (pairs n).length) (w : ℕ) :
    w < n → ∀ (v : Bool) (St : ∀ k, List (Γ k)), St .L = (mkL n w).map Sym.val → St .R = [] →
    St .Rt = [] → St .Y = bits.reverse.map Sym.val → St .Z = [] →
    ∃ v' S', RunLe prog ((w + 1) * (3 * (pairs n).length + 4 * n + 4)) ⟨some .vtx, v, St⟩
        ⟨some .hv, v', S'⟩ ∧
      S' .O = ((List.range (w + 1)).map (vtxNum n bits)).flatMap (fun a => delimit (encodeNat a)) ++
        St .O ∧
      ∀ j, j ≠ .L → j ≠ .R → j ≠ .Rt → j ≠ .Y → j ≠ .Z → j ≠ .O → S' j = St j

Uses 16 · Used by 1

Statement usesStacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · Vertex marks for a vertex · The subset-sum emitter machine · Stack alphabets of the subset-sum emitter · Vertex pairs in encoding order · Vertex numbers of the SUBSET-SUM reduction · Stack alphabet of the SAT verifier · Self-delimiting form of a bitstring · Runs within a step budget

Proof usesTest for the value symbol true (SUBSET-SUM reduction machine) · Testing a popped input bit · Subset-sum emitter: one vertex number · Run of the mark-return loop of the subset-sum emitter · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byRun of the VERTEX-COVER to SUBSET-SUM machine

TheoremOne halving step of the binary conversion (SUBSET-SUM reduction machine)#✓fully proved

Let \(c\) and \(p\) be natural numbers, \(r\) a bit (read as \(0\) or \(1\) in arithmetic), \(v\) a value of the machine's Boolean flag and \(S\) an assignment of contents to the stacks. Suppose stack \(A\) holds \(2c + r\) copies of the unit symbol and stack \(H\) holds \(p\) copies. Then, starting at label \(\mathrm{hv0}\) with flag \(v\) and stacks \(S\), the machine reaches label \(\mathrm{hvB}\) in exactly \(2c + r + 1\) steps, with some flag \(v'\) and stacks \(S'\) such that \(S'(A)\) is empty, \(S'(H)\) holds \(p + c\) copies of the unit symbol, \(S'(T)\) is the input-bit symbol \(\mathrm{bit}(r)\) on top of \(S(T)\), and every stack other than \(A\), \(H\), \(T\) holds the same contents as in \(S\).

theorem hv0_run : ∀ (c : ℕ) (r : Bool) (p : ℕ) (v : Bool) (St : ∀ k, List (Γ k)),
    St .A = cnt U (2 * c + r.toNat) → St .H = cnt U p →
    ∃ v' S', Run prog (2 * c + r.toNat + 1) ⟨some .hv0, v, St⟩ ⟨some .hvB, v', S'⟩ ∧
      S' .A = [] ∧ S' .H = cnt U (p + c) ∧ S' .T = .bit r :: St .T ∧
      ∀ j, j ≠ .A → j ≠ .H → j ≠ .T → S' j = St j

Uses 9 · Used by 1

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 · Exact-length runs of a TM2 machine · Unary counter

Proof usesA single step executes the statement at the current label

Used byBinary conversion (SUBSET-SUM reduction machine)

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.