Emitting a canonical frame in reverse

DefinitionReversed self-delimiting frame emitter#✓fully proved

Emit one raw payload as a reversed self-delimiting frame.

def emitFrame (a b : K) (d : Γ a → Option Bool) (g : Bool → Γ b)
    (self next : Λ) : TM2.Stmt Γ Λ Bool :=
  .peek a (fun _ o => isBit d o) <| .branch id
    (.pop a (fun _ o => bitOf d o) <|
      .push b (fun _ => g true) <| .push b g <| .goto fun _ => self)
    (.push b (fun _ => g false) <| .goto fun _ => next)

Uses 2 · Used by 5

Statement usesBit on top of a stack · Bit test for the top of a stack

Used byProgram of the list-of-naturals canonicalizer · Program of the pair-list projector · Frame emitter takes one step per payload bit plus one · Quadratic run of the raw-input SUBSET-SUM to PARTITION machine · Raw-input PARTITION membership machine runs in quadratic time

TheoremFrame emitter takes one step per payload bit plus one#✓fully proved

Emit a complete frame in payload.length + 1 steps, restoring the input suffix and leaving every unrelated stack unchanged.

theorem emitFrame_run {M : Λ → TM2.Stmt Γ Λ Bool}
    {a b : K} {d : Γ a → Option Bool} {g : Bool → Γ b}
    {self next : Λ} (hM : M self = emitFrame a b d g self next)
    (hab : a ≠ b) (ga : Bool → Γ a) (hga : ∀ c, d (ga c) = some c)
    (payload : List Bool) : ∀ (tail : List (Γ a)) (v : Bool)
      (S : ∀ k, List (Γ k)), EndsBitBlock d tail →
      S a = payload.map ga ++ tail →
      ∃ S', Run M (payload.length + 1) ⟨some self, v, S⟩
        ⟨some next, false, S'⟩ ∧ S' a = tail ∧
        S' b = ((delimit payload).map g).reverse ++ S b ∧
        ∀ k, k ≠ a → k ≠ b → S' k = S k

Uses 7 · Used by 2

Statement usesReversed self-delimiting frame emitter · Self-delimiting form of a bitstring · End of a bit block · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label · Bit on top of a stack · Bit test for the top of a stack

Used byList canonicalizer normalizes one element · Pair-list projector emits one weight and one value frame per item

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.