relocate_guard_holds
DisprovedThe decidable guard in prefix command relocation always holds when all input symbols are below the alphabet bound: taking the first k1 symbols preserves the bound.
Formal statement
import Definitions.Def_CookLevin_Basic
open CookLevin
theorem relocate_guard_holds
{k1 G1 : Nat} {gs : List Symbol}
(h : ∀ s ∈ gs, s < G1) :
∀ i < k1, (gs.take k1)[i]! < G1 := by sorry