CookLevin.seqCompose_machine_split_child_leaf_child

import Definitions.Def_CookLevin_Basic
import Definitions.Def_CookLevin_Satisfiability
import Definitions.Def_CookLevin_Complexity
import Definitions.Def_CookLevin_Reduction

open CookLevin

theorem CookLevin.seqCompose_machine_split_child_leaf_child
    (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