CookLevin.bridge_isFormulaStringB_polyTimeDecidable
ProvedA graph bridge connecting the machine-composition leaves to the accepted isFormulaStringB_polyTimeDecidable sketch.
Formal statement
import Definitions.Def_CookLevin_Basic import Definitions.Def_CookLevin_Satisfiability import Definitions.Def_CookLevin_Complexity import Definitions.Def_CookLevin_Verifier open CookLevin theorem CookLevin.bridge_isFormulaStringB_polyTimeDecidable : True := by sorry