Sequential composition of two multi-tape Turing machines

Open

CookLevin.turingMachine_and_compose

by Mazecto · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theorydecision-proceduresequential-compositionturing-machine

Let $M_1$ and $M_2$ be two multi-tape Turing machines with tape counts $k_1, k_2$ and alphabet bounds $G_1, G_2$ that decide binary predicates $V_1$ and $V_2$ within time bounds $T_1(|x|+|w|)$ and $T_2(|x|+|w|)$ respectively.

Then there exists a composed multi-tape Turing machine $M$ with tape count $k$ and alphabet size $G$ satisfying $\mathrm{TuringMachine}(k, G, M)$ that decides their boolean conjunction:

V(x, w) = V_1(x, w) \wedge V_2(x, w)

within the sum of the two time bounds:

T(x, w) = T_1(|x| + |w|) + T_2(|x| + |w|).

The machine $M$ first runs $M_1$ on the input tapes $(x, w)$ . Upon reaching the halting state of $M_1$ , it inspects cell 1 of the verdict tape: if $M_1$ rejected (symbol $\mathbf{0}$ ), $M$ halts and rejects; if $M_1$ accepted (symbol $\mathbf{1}$ ), $M$ executes $M_2$ and writes $M_2$ 's verdict to the final verdict tape. The total step count is bounded by $T_1 + T_2$ .

This theorem provides the general sequential composition principle for multi-tape Turing machines deciding languages on binary tape inputs.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem turingMachine_and_compose
    (M1 M2 : Machine) (k1 k2 G1 G2 : Nat)
    (hwf1 : TuringMachine k1 G1 M1) (hwf2 : TuringMachine k2 G2 M2)
    (V1 V2 : List Bool → List Bool → Bool)
    (T1 T2 : Nat → Nat)
    (hdec1 : ∀ x w : List Bool, DecidesIn M1 k1 (boolsToSymbols x) (boolsToSymbols w) (T1 (x.length + w.length)) (V1 x w))
    (hdec2 : ∀ x w : List Bool, DecidesIn M2 k2 (boolsToSymbols x) (boolsToSymbols w) (T2 (x.length + w.length)) (V2 x w)) :
    ∃ (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (T1 (x.length + w.length) + T2 (x.length + w.length))
          (V1 x w && V2 x w) := by sorry
end CookLevin

Source

https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Basic.lean#L70

View graph