CookLevin.formulaRoundTrip_transducer_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.formulaRoundTrip_transducer_child_reduction_child :
    ∃ (M : Machine) (k G c1 : Nat),
      TuringMachine k G M ∧
      ComputesInTime M k (fun n => c1 * (n + 1) ^ 2) (fun x => encodeFormula (decodeFormula x)) := by sorry