Sum of polynomial bounds is bounded by a polynomial bound
ProvedpolyBound_sum_leThe sum of two polynomial bounds polyBound c d n + polyBound c' d' n is at most polyBound (c + c') (max d d') n. This is used to combine the time bounds when running two polynomial-time machines in sequence.
Formal statement
import Definitions.Def_CookLevin_Cost
open CookLevin
theorem polyBound_sum_le {c d c' d' n : Nat} :
polyBound c d n + polyBound c' d' n ≤ polyBound (c + c') (max d d') n := by sorry