Time-bounded decision is monotone in the time bound
ProveddecidesIn_monoIf a multi-tape Turing machine M decides a bit b on inputs (xs, ws) within t steps, then it also decides b within any larger number t' of steps. This is because once M reaches its halting state it stays there (the step function is a fixed point at the halting state), so the verdict read at time t persists at all later times.
Formal statement
import Definitions.Def_CookLevin_Cost
open CookLevin
theorem decidesIn_mono {M : Machine} {k : Nat} {xs ws : List Symbol} {t t' : Nat} {b : Bool}
(h : DecidesIn M k xs ws t b) (hle : t ≤ t') : DecidesIn M k xs ws t' b := by sorry