Sequential-composition tail pipeline

This module verifies the pipeline after the first function computation has placed its raw output on the dedicated work tape. The pipeline rewinds that tape, copies its delimited HasOutput value onto a fresh canonical tape, rewinds the fresh tape, and runs the placed started-input wrapper for the second machine. Its final output contract may describe either a computed string or a decision verdict.

The phase-expanded bound is (B + 2) + 1 + (|y| + 1) + 1 + (|y| + 1 + 2) + 1 + G(|y|), which simplifies to B + 2 * |y| + 9 + G(|y|).

def Complexity.TM.CompositionTailPre (nf ng : ℕ) (y : List Bool) (B : ℕ) (inp : Tape) (work : Fin (compositionTapeCount nf ng) → Tape) (out : Tape) : Prop

Boundary contract consumed only by the proof-internal composition tail.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.compositionTailTM_hoareTime_internal {nf ng : ℕ} (tmG : TM ng) {g : List Bool → List Bool} {G : ℕ → ℕ} (hG : tmG.ComputesInTime g G) (y : List Bool) (B : ℕ) : (compositionTailTM nf ng tmG).HoareTime (CompositionTailPre nf ng y B) (fun (_inp : Tape) (_work : Fin (compositionTapeCount nf ng) → Tape) (out : Tape) => out.HasOutput (g y)) (B + 2 + 1 + (y.length + 1 + 1 + (y.length + 1 + 2 + 1 + G y.length)))

The post-first-computation tail correctly runs the second function.

theorem Complexity.TM.compositionTailTM_decides_hoareTime_internal {nf ng : ℕ} (tmG : TM ng) {L : Language} {G : ℕ → ℕ} (hG : tmG.DecidesInTime L G) (y : List Bool) (B : ℕ) : (compositionTailTM nf ng tmG).HoareTime (CompositionTailPre nf ng y B) (fun (_inp : Tape) (_work : Fin (compositionTapeCount nf ng) → Tape) (out : Tape) => (y ∈ L → out.cells 1 = Γ.one) ∧ (y ∉ L → out.cells 1 = Γ.zero)) (B + 2 + 1 + (y.length + 1 + 1 + (y.length + 1 + 2 + 1 + G y.length)))

The same tail pipeline retains a second machine's decision verdict.