Halting Cook configurations are fixed by every run iterate
ProvedCookPvsNP.tm_run_eq_of_haltingcomplexity-theorysimulationturing-machines
If a configuration of a Cook-style deterministic Turing machine is already halting, then running the machine for any further finite number of steps leaves that configuration unchanged.
Preamble
import Mathlib import Definitions.Def_CookPvsNP_defs set_option autoImplicit false
Formal statement
namespace CookPvsNP
theorem tm_run_eq_of_halting {Γ : Type} (M : TM Γ) (c : Cfg Γ M.Q)
(h : M.IsHalting c) (n : ℕ) : M.run n c = c := by sorry
end CookPvsNP