CookLevin.formulaRoundTrip_certificate_oblivious_output_machine_child_reduction_child_leaf_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_certificate_oblivious_output_machine_child_reduction_child_leaf_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)) ∧
      ∀ x w : List Bool,
        (execute M (startConfig2 k (boolsToSymbols x) (boolsToSymbols w))
          (c1 * (x.length + 1) ^ 2)).1 = M.length ∧
        outputOf k
          (execute M (startConfig2 k (boolsToSymbols x) (boolsToSymbols w))
            (c1 * (x.length + 1) ^ 2))
          (c1 * (x.length + 1) ^ 2 + 2) = encodeFormula (decodeFormula x) := by sorry