Prove2Me

CookLevin.cook_levin_theorem_child_sub_child

Proved

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

Child sub-lemma for cook_levin_theorem_child

Formal statement
import Definitions.Def_CookLevin_Verifier
import Definitions.Def_CookLevin_Reduction

open CookLevin

theorem CookLevin.cook_levin_theorem_child_sub_child (h1 : PolyTimeDecidable satVerifier) (h2 : ReductionIsPolyTime) :
    NPComplete SAT := by sorry

View graph