turingCommand_mono
DisprovedThe TuringCommand well-formedness property is monotone in the tape count, state bound, and alphabet size: a command well-formed for smaller bounds is well-formed for larger bounds.
Formal statement
import Definitions.Def_CookLevin_Basic
open CookLevin
theorem turingCommand_mono
{k1 k Q1 Q G1 G : Nat} {cmd : Command}
(hk : k1 ≤ k) (hQ : Q1 ≤ Q) (hG : G1 ≤ G)
(hcmd : TuringCommand k1 Q1 G1 cmd) :
TuringCommand k Q G cmd := by sorry