CookLevin.isFormulaStringB_polyTimeDecidable_child_leaf_child

Open

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

Child lemma for open leaf CookLevin.isFormulaStringB_polyTimeDecidable_child

Formal statement

import Definitions.Def_CookLevin_Verifier

open CookLevin

theorem CookLevin.isFormulaStringB_polyTimeDecidable_child_leaf_child :
    PolyTimeDecidable (fun x _w => isFormulaStringB x) := by sorry

View graph