Cook–Levin machine model: independent computations with retained work banks
ProvedCookLevin.machine_two_independent_computationscomplexity-theorycook-levinturing-machines
Two well-formed machines sharing an alphabet can compute sequentially on the same Boolean input using separate work banks. The combined machine uses k1+k2-1 tapes and takes at most 2*T1+1+T2 steps when the two source transformations take at most T1 and T2. It retains the first final work bank unchanged while producing the second final work bank. The second work bank is represented in reverse index order both initially and finally. This executes the two computations; copying their outputs into one encoded list is a separate remaining step.
Preamble
import Definitions.Def_CookLevin_Cost open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.machine_two_independent_computations {k₁ k₂ G : Nat}
(M₁ M₂ : Machine) (h₁ : TuringMachine k₁ G M₁) (h₂ : TuringMachine k₂ G M₂) :
∃ R : Machine, TuringMachine (k₁ + (k₂ - 1)) G R ∧
∀ (x : List Bool) (work₁ work₂ final₁ final₂ : List Tape)
(finalInput₂ : Tape) (T₁ T₂ : Nat),
work₁.length + 1 = k₁ → work₂.length + 1 = k₂ →
Transforms M₁ ((contents (boolsToSymbols x), 0) :: work₁) T₁ final₁ →
Transforms M₂ ((contents (boolsToSymbols x), 0) :: work₂) T₂
(finalInput₂ :: final₂) →
Transforms R ((contents (boolsToSymbols x), 0) :: (work₁ ++ work₂.reverse))
(2 * T₁ + 1 + T₂) (finalInput₂ :: (final₁.tail ++ final₂.reverse)) := by sorrySource
Composition of the accepted input-reset, tape-padding, separate-work-bank, and machine-sequencing results.