CookLevin.turingMachine_and_compose_wf_child_reduction_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.turingMachine_and_compose_wf_child_reduction_child
    (M1 M2 : Machine) (k1 k2 G1 G2 : Nat)
    (hwf1 : TuringMachine k1 G1 M1) (hwf2 : TuringMachine k2 G2 M2) :
    ∃ (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      ∀ (xs ws : List Symbol) (t1 t2 : Nat) (b1 b2 : Bool),
        DecidesIn M1 k1 xs ws t1 b1 →
        DecidesIn M2 k2 xs ws t2 b2 →
        DecidesIn M k xs ws (t1 + t2) (b1 && b2) := by sorry