Cook–Levin machine model: sequential composition with additive runtime
ProvedCookLevin.machine_sequence_preserves_turing_and_timecomplexity-theorycook-levinturing-machines
Two well-formed multi-tape Turing machines with the same tape count and alphabet can be sequenced by appending the second command list after shifting its state addresses. The explicit combined machine is well formed. If the first machine transforms the initial tapes to intermediate tapes within T1 steps and the second transforms those intermediate tapes to final tapes within T2 steps, the combined machine performs the transformation within T1 + T2 steps. This is a tape-level composition theorem; preparing the intermediate tapes for independently specified string functions is a separate obligation.
Preamble
import Definitions.Def_CookLevin_Basic open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.machine_sequence_preserves_turing_and_time
{k G : Nat} (M₁ M₂ : Machine)
(h₁ : TuringMachine k G M₁) (h₂ : TuringMachine k G M₂) :
let combined : Machine := M₁ ++ M₂.map
(fun cmd gs => (M₁.length + (cmd gs).1, (cmd gs).2))
TuringMachine k G combined ∧
∀ (tps middle finalTps : List Tape) (T₁ T₂ : Nat),
Transforms M₁ tps T₁ middle → Transforms M₂ middle T₂ finalTps →
Transforms combined tps (T₁ + T₂) finalTps := by sorrySource
The existing CookLevin Basic machine semantics, with explicit relocation of state addresses and first-halting-time simulation. Developed for composition in the polynomial-time reduction milestone.