Sequential composition Turing machine with short-circuit reject

Open

CookLevin.seqCompose_machine_split

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

control-flowsequential-compositionshort-circuitturing-machine

Given two multi-tape Turing machines $M_1$ and $M_2$ with tape counts $k_1, k_2$ and alphabet sizes $G_1, G_2$ , there exists a sequential composition machine $M$ with $k$ tapes and alphabet size $G$ satisfying $\mathrm{TuringMachine}(k, G, M)$ that splits into two execution regimes:

Short-circuit Rejection: If $M_1$ rejects ( $b_1 = \mathbf{0}$ ) on $(xs, ws)$ within $t_1$ steps, $M$ halts and writes $\mathbf{0}$ to the verdict tape in $t_1$ steps:

\mathrm{DecidesIn}(M_1, k_1, xs, ws, t_1, \mathrm{false}) \implies \mathrm{DecidesIn}(M, k, xs, ws, t_1, \mathrm{false}).

Sequential Continuation: If $M_1$ accepts ( $b_1 = \mathbf{1}$ ) within $t_1$ steps, $M$ executes $M_2$ on $(xs, ws)$ for $t_2$ steps, producing $M_2$ 's verdict $b_2$ at time $t_1 + t_2$ :

\mathrm{DecidesIn}(M_1, k_1, xs, ws, t_1, \mathrm{true}) \wedge \mathrm{DecidesIn}(M_2, k_2, xs, ws, t_2, b_2) \implies \mathrm{DecidesIn}(M, k, xs, ws, t_1 + t_2, b_2).

This isolates the machine construction and state-transition control flow for sequential boolean conjunction.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem seqCompose_machine_split
    (M1 M2 : Machine) (k1 k2 G1 G2 : Nat) :
    ∃ (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      (∀ (xs ws : List Symbol) (t1 : Nat),
        DecidesIn M1 k1 xs ws t1 false →
        DecidesIn M k xs ws t1 false) ∧
      (∀ (xs ws : List Symbol) (t1 t2 : Nat) (b2 : Bool),
        DecidesIn M1 k1 xs ws t1 true →
        DecidesIn M2 k2 xs ws t2 b2 →
        DecidesIn M k xs ws (t1 + t2) b2) := by sorry
end CookLevin

Source

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

View graph