Part 7 of 7

TheoremEmbedded run of the binary addition component#✓fully proved

The addition component runs in a host, with every external stack unchanged and all embedded workspace cleared.

theorem run_embedded {K Λ : Type} [DecidableEq K] {Γ : K → Type}
    (E : SEmb (fun _ : SSVerify.K => Sym) Γ) (φ : Lab → Λ)
    (M : Λ → TM2.Stmt Γ Λ Bool) (hM : Embeds E φ prog M)
    (m n : ℕ) (v : Bool) (S : ∀ k, List (Γ k))
    (hS : Agree E (SSVerify.st ((pairInput m n).map .bit)
      [] [] [] []) S) :
    let N := (pairInput m n).length
    ∃ v' S', RunLe M (N * (2 * N + 6) + 2 * N + 8)
      ⟨some (φ (.inr 0)), v, S⟩ ⟨some (φ (.inr 3)), v', S'⟩ ∧
      Agree E (SSVerify.st [] [] []
        ((encodeNat (m + n)).map .bit) []) S' ∧ Frame E S S'

structure SEmb {K K' : Type} (Γ : K → Type) (Γ' : K' → Type) where
  /-- The stack renaming. -/
  e : K → K'
  /-- Distinct sub-machine stacks go to distinct host stacks. -/
  inj : Injective e
  /-- The alphabet of each sub-machine stack, identified with its host stack's. -/
  ι : ∀ k, Γ k ≃ Γ' (e k)

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:51

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

CSLibExt/Computability/Complexity/Karp/SubsetSumVerify.lean:299

inductive Sym
  | bit (b : Bool) | lit (p : Bool) | cl | val (b : Bool) | dead
  deriving DecidableEq

CSLibExt/Computability/Complexity/SatVerifierSpec.lean:41

abbrev Lab := SSVerify.Lab ⊕ Fin 4

CSLibExt/Computability/Complexity/SSVerifierArithmetic.lean:65

def Embeds (M : Λ → TM2.Stmt Γ Λ σ) (M' : Λ' → TM2.Stmt Γ' Λ' σ) : Prop :=
  ∀ l, M' (φ l) = mapS E φ (M l) ∨ M l = .halt

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:76

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

CSLibExt/Computability/Complexity/SSVerifierArithmetic.lean:86

def Agree (S : ∀ k, List (Γ k)) (S' : ∀ k', List (Γ' k')) : Prop :=
  ∀ k, S' (E.e k) = (S k).map (E.ι k)

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:80

def st (x w t a b : List Sym) : K → List Sym
  | .X => x
  | .W => w
  | .T => t
  | .A => a
  | .B => b
  | .P => []
  | .Q => []

CSLibExt/Computability/Complexity/Karp/SubsetSumVerify.lean:376

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

CSLibExt/Computability/Complexity/SSVerifierArithmetic.lean:61

def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  ∃ n, n ≤ B ∧ Run M n c d

MathlibExt/Computability/TuringMachine/Program.lean:901

def Frame (S' S'' : ∀ k', List (Γ' k')) : Prop :=
  ∀ k', (∀ k, E.e k ≠ k') → S'' k' = S' k'

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:84

Uses 14

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 · 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 usesBinary addition of framed numbers in quadratic time · Run embedding for bounded runs

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.