Turing machine well-formedness is preserved under command mapping
ProvedturingMachine_mapThe TuringMachine well-formedness property is preserved under mapping a command-transforming function over the machine, provided the function preserves the TuringCommand property for each command (with the mapped machine length).
Formal statement
import Definitions.Def_CookLevin_Basic
open CookLevin
theorem turingMachine_map
{k G : Nat} {M : Machine} {f : Command → Command}
(hM : TuringMachine k G M)
(hf : ∀ cmd ∈ M, TuringCommand k (M.map f).length G (f cmd)) :
TuringMachine k G (M.map f) := by sorry