Polynomial complexity bound for tableau reduction emitter
ProvedCookLevin.reductionEmitM_polyBoundcomplexity-boundcook-levinreduction
The step count of the reduction emitter machine is bounded by a polynomial in the input length.
Formal statement
import Definitions.Def_CookLevin_Basic
import Definitions.Def_CookLevin_Satisfiability
import Definitions.Def_CookLevin_Complexity
import Definitions.Def_CookLevin_Reduction
open CookLevin
theorem CookLevin.reductionEmitM_polyBound (cw dw ct dt : Nat) :
∃ c d : Nat, ∀ n : Nat, n + cw + dw + ct + dt ≤ polyBound c d n := by sorry
Source