The summing loop of the SUBSET-SUM verifier to Binary addition of framed numbers in quadratic time

TheoremThe summing loop of the SUBSET-SUM verifier#✓fully proved

Let \(N\) be a natural number and \(t\) a list of symbols. Write \(\langle m \rangle\) for the canonical binary code of a natural number \(m\), least significant bit first, and put a bit list on a stack as the list of its name-bit symbols. Let \(n\) and \(s\) be natural numbers, \(r\) and \(w\) bit lists and \(v\) a Boolean, with \(|r| \le n\) and \(|\langle s \rangle| + |r| \le N\). Start the SUBSET-SUM verifier at the label \(\mathsf{next}\) with internal state \(v\), with \(r\) on \(X\), \(w\) on \(W\), \(t\) on \(T\), \(\langle s \rangle\) on \(A\), and the stacks \(B\), \(P\) and \(Q\) empty. Then for some internal state \(v'\) and stack contents \(S'\) it runs within \(|r| \cdot (2N + 6) + 1\) steps to the configuration with internal state \(v'\), stacks \(S'\) and label \(\mathsf{fmove}\) if parsing the number blocks of \(r\) with fuel \(n\) succeeds, and label \(\mathsf{no}\) if it fails. Moreover, if that parsing gives the list of numbers \(a\), and \(\sigma\) is \(s\) plus the sum of the numbers of \(a\) chosen by the mask \(w\), then \(|\langle \sigma \rangle| \le N\), and for some list of symbols \(w'\) the stacks \(S'\) hold nothing on \(X\), \(w'\) on \(W\), \(t\) on \(T\), \(\langle \sigma \rangle\) on \(A\), and nothing on \(B\), \(P\) and \(Q\).

theorem loop_run (N : ℕ) (t : List Sym) : ∀ (n : ℕ) (r w : List Bool) (s : ℕ) (v : Bool),
    r.length ≤ n → (encodeNat s).length + r.length ≤ N →
    ∃ v' S', RunLe prog (r.length * (2 * N + 6) + 1)
      ⟨some .next, v, st (r.map .bit) (w.map .bit) t ((encodeNat s).map .bit) []⟩
      ⟨some (if (numsAux n r).isSome then .fmove else .no), v', S'⟩ ∧
      ∀ as, numsAux n r = some as → (encodeNat (s + (pick as w).sum)).length ≤ N ∧
        ∃ w', S' = st [] w' t ((encodeNat (s + (pick as w).sum)).map .bit) []

Uses 30 · Used by 2

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Parsing number blocks, with fuel · Numbers chosen by a mask · The SUBSET-SUM verifier program · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesRejection by the SUBSET-SUM verifier within a step bound · 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 · Moving the new sum back · Carry bit of a full adder · Canonical binary strings are those not ending in zero · Adding a carry bit · Whether a bit string ends in false · The verifier rejects an unterminated skipped block · Skipping a number block · Reading a symbol as a name bit · 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 · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack

Used byThe SUBSET-SUM verifier machine · SUBSET-SUM verifier computes the mask-selected sum

TheoremCubic bound on the verifier's phase costs#✓fully proved

For natural numbers \(X\), \(W\), \(P\), \(R\) and \(S\) with \(P + R \le X\) and \(S \le X\), \(P + 1 + (R(2X + 6) + 1) + (S + 1) + (S + 1) \le 16 (X + W + 1)^3\).

theorem cost_le (X W P R S : ℕ) (hP : P + R ≤ X) (hS : S ≤ X) :
    P + 1 + (R * (2 * X + 6) + 1) + (S + 1) + (S + 1) ≤ 16 * (X + W + 1) ^ 3

Used by 1

Used byThe SUBSET-SUM verifier machine

TheoremThe SUBSET-SUM verifier machine#✓fully proved

Let \(x\) and \(w\) be lists of bits and \(v\) a Boolean, and let \(S\) assign stack contents with the bits of \(x\) on \(X\), the bits of \(w\) on \(W\) and every other stack empty. Started at the start label with internal state \(v\) and stacks \(S\), the verifier program reaches, within \(16(|x| + |w| + 1)^3\) steps, a configuration with label \(\mathsf{yes}\) if the SUBSET-SUM check accepts \((x, w)\), and with label \(\mathsf{no}\) otherwise.

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

Uses 27 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · The SUBSET-SUM verifier · Start state of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesRejection by the SUBSET-SUM verifier within a step bound · Comparing the sum with the target · Cubic bound on the verifier's phase costs · Decoding a SUBSET-SUM instance · Canonical binary strings are those not ending in zero · Moving the final sum for the comparison · Whether a bit string ends in false · The summing loop of the SUBSET-SUM verifier · Parsing number blocks, with fuel · Numbers chosen by a mask · Stack contents of the SUBSET-SUM verifier · The verifier rejects an unterminated target block · Reading the target block · The binary code of natural numbers is injective · 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 · Exact-length runs of a TM2 machine

Used bySUBSET-SUM is in NP

AbbreviationThe SUBSET-SUM verifier machine as a host component#✓fully proved

The multi-stack Turing machine that checks SUBSET-SUM certificates, packaged as a host component: it has seven stacks, each holding symbols of the SAT verifier alphabet, its labels and its program are those of the machine, and the list of its stacks names each of the seven stacks exactly once.

abbrev ssVerifyComp : Host.Comp where
  K := SSVerify.K
  Γ := fun _ => SatVerifier.Sym
  finΓ := fun _ => SatVerifier.Sym.instFintype
  L := SSVerify.Lab
  prog := SSVerify.prog
  ks := [.X, .W, .T, .A, .B, .P, .Q]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide

Uses 5 · Used by 1

Statement usesComponent machine · Stacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Stack alphabet of the SAT verifier

Used bySUBSET-SUM is in NP

TheoremSUBSET-SUM is in NP#✓fully proved

SUBSET-SUM is the decision problem on bit strings that accepts \(x\) exactly when \(x\) encodes a target \(t\) followed by natural numbers \(a_1, \dots, a_n\) (each written in binary and delimited) such that some, possibly empty, sublist of \(a_1, \dots, a_n\) sums to \(t\). This decision problem belongs to NP: there are a polynomial \(p\) with natural-number coefficients and a polynomial-time computable verifier \(R\) such that SUBSET-SUM accepts \(x\) exactly when \(R(x, w)\) holds for some bit string \(w\) with \(|w| \le p(|x|)\).

theorem subsetSumDec_mem_NP : subsetSumDec ∈ NP

Uses 26 · Used by 2

Statement usesThe SUBSET-SUM problem · Complexity classes · Decision problems · The complexity class NP

Proof usesComponent machine · Verifier host, canonical form · Stacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · The SUBSET-SUM verifier machine · The SUBSET-SUM verifier · Start state of the SUBSET-SUM verifier · SUBSET-SUM is characterized by its verifier · The SUBSET-SUM verifier machine as a host component · Stack alphabet of the SAT verifier · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions · Exact-length runs of a TM2 machine · Runs within a step budget

Used byBinary-coded PARTITION is in NP · SUBSET-SUM is NP-complete

AbbreviationThe VERTEX-COVER to SUBSET-SUM machine as a host component#✓fully proved

The multi-stack Turing machine that computes the VERTEX-COVER to SUBSET-SUM reduction on bit strings, packaged as a host component: its fifteen stacks (the output stack holds booleans, every other stack holds symbols of the SAT verifier alphabet), its labels and its program are those of the machine, and the list of its stacks names each of the fifteen stacks exactly once.

abbrev emitSSComp : Host.Comp where
  K := EmitSS.K
  Γ := EmitSS.Γ
  L := EmitSS.Lab
  prog := EmitSS.prog
  ks := [.X, .O, .A, .H, .N, .M, .C, .S1, .S2, .Y, .Z, .T, .L, .R, .Rt]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide

Uses 6 · Used by 1

Statement usesComponent machine · Stacks 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

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

TheoremThe VERTEX-COVER to SUBSET-SUM reduction is polynomial-time#✓fully proved

The reduction map on bit strings, which sends the encoding of a VERTEX-COVER instance \((k, G)\) to the encoding of the SUBSET-SUM instance built from it (one base-4 number for each vertex and for each pair of vertices of \(G\), and a target) and every other bit string to the instance with no numbers and target \(1\), is computable in polynomial time.

theorem isPolyTime_reduceSS : IsPolyTime reduceSS

Uses 22 · Used by 1

Statement usesReduction from VERTEX-COVER to SUBSET-SUM · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions

Proof usesComponent machine · Reduction host, canonical form · Stacks of the SUBSET-SUM reduction machine · Labels of the subset-sum emitter · The subset-sum emitter machine · Run of the VERTEX-COVER to SUBSET-SUM machine · Start label of the subset-sum emitter · Stack alphabets of the subset-sum emitter · The VERTEX-COVER to SUBSET-SUM machine as a host component · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine · Runs within a step budget

Used bySUBSET-SUM is NP-hard

TheoremSUBSET-SUM is NP-hard#✓fully proved

Let SUBSET-SUM be the decision problem on bit strings that accepts exactly the strings encoding a target \(t\) followed by natural numbers \(a_1, \dots, a_n\) (each written in binary and delimited) such that some, possibly empty, sublist of \(a_1, \dots, a_n\) sums to \(t\). Every decision problem \(L\) in NP reduces to SUBSET-SUM by a polynomial-time many-one reduction: there is a polynomial-time computable map \(f\) on bit strings such that, for every bit string \(x\), \(L\) accepts \(x\) exactly when SUBSET-SUM accepts \(f(x)\).

theorem subsetSumDec_npHard : ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L subsetSumDec

Uses 32 · Used by 2

Statement usesThe SUBSET-SUM problem · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP

Proof usesDecoding a graph instance · Encoding of a graph instance · Bit-string encoding of SUBSET-SUM instances · Vertex covers of size \(k\) match subset sums hitting the target · The VERTEX-COVER to SUBSET-SUM reduction is polynomial-time · Language of graph instances with a property · Unparsable input is rejected · Fixed no-instance of SUBSET-SUM · NP-hardness transfers along reductions · Vertex pairs in encoding order · Reduction from VERTEX-COVER to SUBSET-SUM · Numbers of the SUBSET-SUM reduction · Target of the SUBSET-SUM reduction · The fixed no-instance of SUBSET-SUM · The graph encoded by pair bits · The VERTEX-COVER problem · VERTEX-COVER (exact size k) is NP-hard · Reading a unary length prefix · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions

Used byPARTITION is NP-complete · SUBSET-SUM is NP-complete

TheoremSUBSET-SUM is NP-complete#✓fully proved

Let SUBSET-SUM be the decision problem on bit strings that accepts exactly the strings encoding a target \(t\) followed by natural numbers \(a_1, \dots, a_n\) (each written in binary and delimited) such that some, possibly empty, sublist of \(a_1, \dots, a_n\) sums to \(t\). Then SUBSET-SUM belongs to NP, and every decision problem \(L\) in NP reduces to SUBSET-SUM by a polynomial-time many-one reduction: there is a polynomial-time computable map \(f\) on bit strings such that, for every bit string \(x\), \(L\) accepts \(x\) exactly when SUBSET-SUM accepts \(f(x)\).

theorem subsetSumDec_npComplete :
    subsetSumDec ∈ NP ∧ ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L subsetSumDec

Uses 7

Statement usesThe SUBSET-SUM problem · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP

Proof usesSUBSET-SUM is in NP · SUBSET-SUM is NP-hard

TheoremSUBSET-SUM verifier computes the mask-selected sum#✓fully proved

On canonical delimited encodeNat blocks, the existing component leaves the selected sum at a halt label. Normalize raw payloads first: malformed blocks can instead reject early, leaving only a partial sum. The cost uses framed bit length, never numeric magnitudes. The mask is consumed; copy it before reuse in another component.

theorem sum_component_run (as : List ℕ) (w : List Bool) (v : Bool) :
    let r := as.flatMap fun a =>
      BitstringEncoding.delimit (Computability.encodeNat a)
    let bits := Computability.encodeNat (SSVerify.pick as w).sum
    ∃ v' w', RunLe SSVerify.prog
      (r.length * (2 * r.length + 6) + r.length + 3)
      ⟨some .next, v, SSVerify.st (r.map .bit) (w.map .bit) [] [] []⟩
      ⟨some (if bits = [] then .yes else .no), v',
        SSVerify.st [] w' [] [] (bits.map .bit).reverse⟩

Uses 22 · Used by 2

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Numbers chosen by a mask · The SUBSET-SUM verifier program · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Self-delimiting form of a bitstring · Runs within a step budget

Proof usesCanonical binary strings are those not ending in zero · Moving the final sum for the comparison · Whether a bit string ends in false · The summing loop of the SUBSET-SUM verifier · Parsing number blocks, with fuel · Reading a symbol as a name bit · Decoding a prefix-coded natural number · Prefix-free code of a natural number · Parsing a self-delimiting block · Parsing one self-delimiting block · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack

Used byBinary addition of framed numbers in quadratic time · Embedded SUBSET-SUM summing component reaches the mapped label

TheoremA long enough all-true mask selects the whole list#✓fully proved

A mask long enough to select every item gives the original list.

theorem pick_all (as : List ℕ) (n : ℕ) (h : as.length ≤ n) :
    SSVerify.pick as (List.replicate n true) = as

Uses 1 · Used by 2

Statement usesNumbers chosen by a mask

Used byQuadratic run of the padding machine on canonical instances · Canonical PARTITION membership transducer runs in quadratic time

TheoremEmbedded SUBSET-SUM summing component reaches the mapped label#✓fully proved

Reach the common mapped label after summing canonical encodeNat blocks; unembedded stacks remain intact. The input agreement requires prior normalization. A raw parse-failure exit can expose a partial sum. This is only a reachability guarantee: hφ does not make the endpoint fresh, distinct from mapped live labels, or a halt of the host. Callers must establish their intended label separation and the code run next. The embedded mask is consumed; each later sum needs its own saved copy.

Cslib.Complexity.SSVerifierSum.sum_embed · 15 lines

theorem sum_embed {K Λ : Type} [DecidableEq K] {Γ : K → Type}
    (E : SEmb (fun _ : SSVerify.K => Sym) Γ)
    (φ : SSVerify.Lab → Λ) (M : Λ → TM2.Stmt Γ Λ Bool)
    (hM : Embeds E φ SSVerify.prog M) (hφ : φ .yes = φ .no)
    (as : List ℕ) (w : List Bool) (v : Bool) (S : ∀ k, List (Γ k))
    (hS : Agree E (SSVerify.st
      ((as.flatMap fun a => BitstringEncoding.delimit
        (Computability.encodeNat a)).map .bit) (w.map .bit) [] [] []) S) :
    let n := (as.flatMap fun a => BitstringEncoding.delimit
      (Computability.encodeNat a)).length
    ∃ v' w' S', RunLe M (n * (2 * n + 6) + n + 3)
      ⟨some (φ .next), v, S⟩ ⟨some (φ .yes), v', S'⟩ ∧
      Agree E (SSVerify.st [] w' [] []
        ((Computability.encodeNat (SSVerify.pick as w).sum).map
          .bit).reverse) S' ∧ Frame E S S'

Uses 14 · Used by 2

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Numbers chosen by a mask · The SUBSET-SUM verifier program · Stack contents of the SUBSET-SUM verifier · Stack alphabet of the SAT verifier · Self-delimiting form of a bitstring · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Runs within a step budget

Proof usesSUBSET-SUM verifier computes the mask-selected sum · Run embedding for bounded runs

Used byQuadratic run of the padding machine on canonical instances · Canonical PARTITION membership transducer runs in quadratic time

DefinitionFramed input of two natural numbers#✓fully proved

Two canonical Nat blocks in the existing list framing.

def pairInput (m n : ℕ) : List Bool :=
  delimit (encodeNat m) ++ delimit (encodeNat n)

Uses 1 · Used by 3

Statement usesSelf-delimiting form of a bitstring

Used byBit length of the sum is at most the input length · Binary addition of framed numbers in quadratic time · Embedded run of the binary addition component

AbbreviationLabels of the binary addition machine#✓fully proved

Original verifier labels plus initialization, clear, reverse, and halt.

abbrev Lab := SSVerify.Lab ⊕ Fin 4

Uses 1 · Used by 5

Statement usesLabels of the SUBSET-SUM verifier

Used byBinary addition program built on the SUBSET-SUM machine · Redirection of the verifier's halt labels · Only halt labels are redirected to the cleanup label · Binary addition of framed numbers in quadratic time · Embedded run of the binary addition component

DefinitionIdentity embedding of the verifier stacks#✓fully proved

Reuse all original verifier stacks without re-encoding symbols.

def identity : SEmb (fun _ : SSVerify.K => Sym)
    (fun _ : SSVerify.K => Sym) where
  e := id
  inj := injective_id
  ι _ := Equiv.refl _

Uses 3 · Used by 2

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

Used byBinary addition program built on the SUBSET-SUM machine · Binary addition of framed numbers in quadratic time

DefinitionRedirection of the verifier's halt labels#✓fully proved

Redirect the two halt labels, leaving every live label distinct.

def redirect : SSVerify.Lab → Lab
  | .yes | .no => .inr 1
  | l => .inl l

Uses 2 · Used by 3

Statement usesLabels of the SUBSET-SUM verifier · Labels of the binary addition machine

Used byBinary addition program built on the SUBSET-SUM machine · Only halt labels are redirected to the cleanup label · Binary addition of framed numbers in quadratic time

TheoremOnly halt labels are redirected to the cleanup label#✓fully proved

The cleanup continuation cannot alias any live verifier label.

@[simp] theorem redirect_eq_clear_iff (l : SSVerify.Lab) :
    redirect l = .inr 1 ↔ l = .yes ∨ l = .no

Uses 3

Statement usesLabels of the SUBSET-SUM verifier · Labels of the binary addition machine · Redirection of the verifier's halt labels

DefinitionBinary addition program built on the SUBSET-SUM machine#✓fully proved

Run the existing sum machine, then clear the mask and restore LSB order. Only the original halt labels are redirected to a continuation.

def prog : Lab → TM2.Stmt (fun _ : SSVerify.K => Sym) Lab Bool
  | .inl l => mapS identity redirect (SSVerify.prog l)
  | .inr i =>
    if i = 0 then
      .push .W (fun _ => .bit true) <|
        .push .W (fun _ => .bit true) <| .goto fun _ => .inl .next
    else if i = 1 then
      cleanS [.W] (.inr 1) (.inr 2)
    else if i = 2 then
      moveB .B .A Sym.bit? Sym.bit (.inr 2) (.inr 3)
    else .halt

Uses 12 · Used by 2

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · The SUBSET-SUM verifier program · Labels of the binary addition machine · Identity embedding of the verifier stacks · Redirection of the verifier's halt labels · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Translating a statement along a stack embedding · Flag bit of a machine state · Cleanup round · Bit-moving loop

Used byBinary addition of framed numbers in quadratic time · Embedded run of the binary addition component

TheoremBit length of the sum is at most the input length#✓fully proved

The canonical sum fits within the two framed operands' bit length.

theorem length_sum_le_input (m n : ℕ) :
    (encodeNat (m + n)).length ≤ (pairInput m n).length

Uses 6 · Used by 1

Statement usesFramed input of two natural numbers

Proof usesRipple-carry addition of bit lists · Addition is correct on canonical numbers · Carry bit of a full adder · Adding a carry bit · Self-delimiting form of a bitstring

Used byBinary addition of framed numbers in quadratic time

TheoremBinary addition of framed numbers in quadratic time#✓fully proved

Add two canonically framed numbers, leaving only the LSB-first result. The bound is quadratic in encoded input length; no loop enumerates values.

theorem run (m n : ℕ) (v : Bool) :
    let N := (pairInput m n).length
    ∃ v', RunLe prog (N * (2 * N + 6) + 2 * N + 8)
      ⟨some (.inr 0), v,
        SSVerify.st ((pairInput m n).map .bit) [] [] [] []⟩
      ⟨some (.inr 3), v',
        SSVerify.st [] [] [] ((encodeNat (m + n)).map .bit) []⟩

Uses 34 · Used by 1

Statement usesStacks of the SUBSET-SUM verifier · Labels of the SUBSET-SUM verifier · Stack contents of the SUBSET-SUM verifier · Labels of the binary addition machine · Framed input of two natural numbers · Binary addition program built on the SUBSET-SUM machine · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesAdding one payload bit to the sum · Carry bit of a full adder · Numbers chosen by a mask · The SUBSET-SUM verifier program · Identity embedding of the verifier stacks · Bit length of the sum is at most the input length · Redirection of the verifier's halt labels · SUBSET-SUM verifier computes the mask-selected sum · Reading a symbol as a name bit · Self-delimiting form of a bitstring · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Run embedding for bounded runs · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Bit on top of a stack · Cleanup round · Cleanup empties its stacks · Bit test for the top of a stack · A halted run stays halted · Bit-moving loop · Running the bit-moving loop

Used byEmbedded run of the binary addition component

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.