Sum-bound multi-tape machine for conjunction of poly-time decidable relations

import Definitions.Def_CookLevin_Basic
import Definitions.Def_CookLevin_Satisfiability
import Definitions.Def_CookLevin_Complexity
import Definitions.Def_CookLevin_Verifier

open CookLevin

theorem CookLevin.polyTimeDecidable_and_sum_core (f g : List Bool → List Bool → Bool)
    (hf : PolyTimeDecidable f) (hg : PolyTimeDecidable g) :
    ∃ (M : Machine) (k G c1 d1 c2 d2 : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (polyBound c1 d1 (x.length + w.length) + polyBound c2 d2 (x.length + w.length))
          (f x w && g x w) := by sorry