CookLevin.formulaRoundTrip_transducer_fixed_child_reduction_child_leaf_child

import Definitions.Def_CookLevin_Verifier

open CookLevin

theorem CookLevin.formulaRoundTrip_transducer_fixed_child_reduction_child_leaf_child :
    ∃ (M : Machine) (k G c1 : Nat),
      TuringMachine k G M ∧
      ∀ 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