Core command construction for sequential composition machine

Open

CookLevin.seqCompose_machine_core

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

command-constructioncontrol-flowsequential-compositionturing-machine

Given constituent machines $M_1, M_2$ and dimensions $(k, G)$ satisfying $2 \le k$ , $k \ge \max(k_1, k_2)$ and $4 \le G$ , $G \ge \max(G_1, G_2)$ , there exists a list of commands $M$ such that every command is well-formed under TuringCommand k M.length G cmd and satisfies the two execution regimes:

If $M_1$ decides $\mathbf{0}$ within $t_1$ steps, $M$ halts with $\mathbf{0}$ within $t_1$ steps.
If $M_1$ decides $\mathbf{1}$ within $t_1$ steps and $M_2$ decides $b_2$ within $t_2$ steps, $M$ halts with $b_2$ within $t_1 + t_2$ steps.

Preamble

import Definitions.Def_CookLevin_Cost

Formal statement

namespace CookLevin
theorem seqCompose_machine_core
    (M1 M2 : Machine) (k1 k2 G1 G2 : Nat) (k G : Nat)
    (hk : 2 ≤ k ∧ k ≥ max k1 k2) (hG : 4 ≤ G ∧ G ≥ max G1 G2) :
    ∃ (M : Machine),
      (∀ cmd ∈ M, TuringCommand k M.length G cmd) ∧
      (∀ (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