Relocated command single-step preserves next-state via machine semantics

Proved

sem_relocate_state

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

Running the relocated command through the machine semantics (sem) yields the same next-state as running the original command on the prefix tapes. This connects the syntactic relocation to the operational semantics.

Formal statement

import Definitions.Def_CookLevin_Basic

open CookLevin

theorem sem_relocate_state {k1 k G1 : Nat} {cmd : Command} {cfg : Config}
    (hguard : ∀ i < k1, ((read cfg.2).take k1)[i]! < G1) :
    (sem (fun gs => 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)))) cfg).1 = (cmd ((read cfg.2).take k1)).1 := by sorry

View graph