CookLevin.isFormulaStringB_machine_from_transducer_comparator_child_reduction_child

import Definitions.Def_CookLevin_Basic
import Definitions.Def_CookLevin_Satisfiability
import Definitions.Def_CookLevin_Complexity
import Definitions.Def_CookLevin_Reduction

open CookLevin

theorem CookLevin.isFormulaStringB_machine_from_transducer_comparator_child_reduction_child :
    ∃ (M : Machine) (k G c : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (c * (x.length + 1) ^ 2)
          (decide (encodeFormula (decodeFormula x) = x)) := by sorry