Sequential composition machine for conjunction

Disproved

CookLevin.turingMachine_seqCompose

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

Given two machines, there is a machine that runs the first to completion, then the second, and outputs the conjunction of their verdicts within the sum of their time bounds.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

import Definitions.Def_CookLevin_Cost
namespace CookLevin
theorem turingMachine_seqCompose
    (M1 M2 : Machine) (k1 k2 G1 G2 : Nat)
    (V1 V2 : List Bool -> List Bool -> Bool)
    (T1 T2 : Nat -> Nat) :
    Exists (fun (M : Machine) => Exists (fun (k : Nat) => Exists (fun (G : Nat) =>
      TuringMachine k G M /\
      forall (x w : List Bool) (b1 b2 : Bool),
        DecidesIn M1 k1 (boolsToSymbols x) (boolsToSymbols w) (T1 (x.length + w.length)) b1 ->
        DecidesIn M2 k2 (boolsToSymbols x) (boolsToSymbols w) (T2 (x.length + w.length)) b2 ->
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (T1 (x.length + w.length) + T2 (x.length + w.length)) (b1 && b2)))) := by sorry
end CookLevin

Source

Decomposition of CookLevin.turingMachine_and_compose, Prove2Me Cook-Levin mission

View graph