CookLevin.decodeCnf_evaluate_machine_bounded_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.decodeCnf_evaluate_machine_bounded_reduction_child :
    ∃ (M : Machine) (c : Nat),
      TuringMachine 6 4 M ∧
      ∀ x w : List Bool,
        DecidesIn M 6 (boolsToSymbols x) (boolsToSymbols w)
          (c * (x.length + 1) * (w.length + 1))
          ((decodeFormula x).all (fun clause =>
            clause.any (fun lit => match lit with
              | Literal.Neg n => !(w.getD n false)
              | Literal.Pos n => w.getD n false))) := by sorry