CookLevin.satisfiesB_polyTimeDecidable_core_reduction_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.satisfiesB_polyTimeDecidable_core_reduction_child :
    ∃ 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)) (satisfiesB (decodeAssignment w) (decodeFormula x)) := by sorry