Relocated command preserves prefix actions and stays on suffix tapes

Proved

relocate_actions

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

The prefix-relocated command produces the original actions on the prefix tapes plus Stay actions on the suffix tapes, when the alphabet guard holds.

Formal statement

import Definitions.Def_CookLevin_Basic

open CookLevin

theorem relocate_actions
    {k1 k G1 : Nat} {cmd : Command} {gs : List Symbol}
    (hguard : ∀ i < k1, (gs.take k1)[i]! < G1) :
    ((if _h : ∀ i < k1, (gs.take k1)[i]! < G1 then
        ((cmd (gs.take k1)).1,
         (cmd (gs.take k1)).2 ++ (List.range (k - k1)).map (fun j => (gs[k1 + j]!, Direction.Stay)))
      else
        (0, gs.map (fun s => (s, Direction.Stay)))) : Nat × List Action).2 =
      (cmd (gs.take k1)).2 ++ (List.range (k - k1)).map (fun j => (gs[k1 + j]!, Direction.Stay)) := by sorry

View graph