CookLevin.satisfiesB_machine_product_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_machine_product_core_reduction_child :
    ∃ (M : Machine) (c1 : Nat),
      TuringMachine 6 4 M ∧
      ∀ x w : List Bool,
        DecidesIn M 6 (boolsToSymbols x) (boolsToSymbols w)
          (c1 * (x.length + 1) * (w.length + 1))
          (satisfiesB (decodeAssignment w) (decodeFormula x)) := by sorry