CookLevin.cook_levin_theorem_child_sub_child_leaf_v2

Proved

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

Sub-leaf lemma for cook_levin_theorem_child_sub_child_leaf

Formal statement

import Definitions.Def_CookLevin_Verifier
import Definitions.Def_CookLevin_Reduction

open CookLevin

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

View graph