Prove2Me

CookLevin.formulaRoundTrip_unary_transducer_child_reduction_child_leaf_child

Open

by Rizwan · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

Child lemma for open leaf CookLevin.formulaRoundTrip_unary_transducer_child_reduction_child

Formal statement
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_unary_transducer_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)) := by sorry

View graph