Cook–Levin machines: concatenate output tapes in linear time
ProvedCookLevin.machine_concatenate_output_tapescomplexity-theorycook-levinturing-machines
For every n and alphabet G >= 4, there is a well-formed (n+4)-tape machine that concatenates two terminated source bit prefixes onto a fresh blank destination. Tape order is input, first source, destination, second source, then n saved tapes. All three active heads start at zero. If the sources encode xs and ys starting at cell one, each followed by a non-bit symbol, the machine halts within |xs|+|ys|+3 steps with the destination equal to the complete standard encoding contents(boolsToSymbols(xs++ys)). This specifies its start marker, all bits, and the entire blank tail. Both source contents are preserved, their heads advance to the terminating cells, and the input and saved tapes retain contents and heads.
Preamble
import Definitions.Def_CookLevin_Cost open CookLevin set_option autoImplicit false
Formal statement
theorem CookLevin.machine_concatenate_output_tapes {n G : Nat} (hG : 4 ≤ G) :
∃ R : Machine, TuringMachine (n + 4) G R ∧
∀ (xs ys : List Bool) (input : Tape) (f g : Nat → Symbol) (saved : List Tape),
saved.length = n →
(∀ j, (hj : j < xs.length) → f (1 + j) = boolSym (xs[j])) →
(¬ (f (1 + xs.length) = zeroSymbol ∨ f (1 + xs.length) = oneSymbol)) →
(∀ j, (hj : j < ys.length) → g (1 + j) = boolSym (ys[j])) →
(¬ (g (1 + ys.length) = zeroSymbol ∨ g (1 + ys.length) = oneSymbol)) →
Transforms R (input :: (f, 0) :: (contents [], 0) :: (g, 0) :: saved)
(xs.length + ys.length + 3)
(input :: (f, 1 + xs.length) ::
(contents (boolsToSymbols (xs ++ ys)), 1 + xs.length + ys.length) ::
(g, 1 + ys.length) :: saved) := by sorrySource
Direct machine construction from CookLevin Basic/Cost: prepare three heads, copy the first prefix, then run a tape-permuted second copier. Composed using the accepted machine_sequence_preserves_turing_and_time theorem.