Prove2Me

CookLevin.polyTime_encodeFormula_append_core_reduction_child

Proved

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

Reduction child lemma for CookLevin.polyTime_encodeFormula_append_core

Formal statement
import Definitions.Def_CookLevin_Reduction
open CookLevin

theorem CookLevin.polyTime_encodeFormula_append_core_reduction_child (f g : List Bool → Formula)
    (hf : IsPolyTimeComputable (fun x => encodeFormula (f x)))
    (hg : IsPolyTimeComputable (fun x => encodeFormula (g x))) :
    IsPolyTimeComputable (fun x => encodeFormula (f x ++ g x)) := by sorry

View graph