CookLevin.polyTimeDecidable_and_core_machine_leaf_child

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_core_machine_leaf_child (f g : List Bool → List Bool → Bool)
    (hf : PolyTimeDecidable f) (hg : PolyTimeDecidable g) :
    ∃ M k G c d, TuringMachine k G M ∧ ∀ x w : List Bool, DecidesIn M k (boolsToSymbols x) (boolsToSymbols w) (polyBound c d (x.length + w.length)) (f x w && g x w) := by sorry