CookLevin.transducer_decider_pipeline_general_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.transducer_decider_pipeline_general_child_reduction_child
    (f : List Bool → List Bool → List Bool)
    (P : List Bool → List Bool → List Bool → Bool)
    (T1 T2 : Nat → Nat)
    (M1 : Machine) (k1 G1 : Nat) (hwf1 : TuringMachine k1 G1 M1)
    (htrans : ∀ x w : List Bool,
      (execute M1 (startConfig2 k1 (boolsToSymbols x) (boolsToSymbols w)) (T1 x.length)).1 = M1.length ∧
      outputOf k1 (execute M1 (startConfig2 k1 (boolsToSymbols x) (boolsToSymbols w)) (T1 x.length))
        (T1 x.length + 2) = f x w)
    (M2 : Machine) (k2 G2 : Nat) (hwf2 : TuringMachine k2 G2 M2)
    (hdec : ∀ x w y : List Bool,
      DecidesIn M2 k2 (boolsToSymbols x) (boolsToSymbols y) (T2 x.length) (P x w y)) :
    ∃ (M : Machine) (k G : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (T1 x.length + T2 x.length) (P x w (f x w)) := by sorry