CookLevin.transducer_pipe_decider_core_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.transducer_pipe_decider_core_child_leaf_child
    (M1 : Machine) (k1 G1 : Nat) (hwf1 : TuringMachine k1 G1 M1)
    (M2 : Machine) (k2 G2 : Nat) (hwf2 : TuringMachine k2 G2 M2) :
    ∃ (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      ∀ (xs ws : List Symbol) (T1 T2 : Nat) (y : List Bool) (b : Bool),
        (execute M1 (startConfig2 k1 xs ws) T1).1 = M1.length →
        outputOf k1 (execute M1 (startConfig2 k1 xs ws) T1) (T1 + 2) = y →
        DecidesIn M2 k2 xs (boolsToSymbols y) T2 b →
        DecidesIn M k xs ws (T1 + T2) b := by sorry