Prove2Me

Relocated command preserves the original next-state

Proved
relocate_nextstate

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

The prefix-relocated command preserves the next-state of the original command when the alphabet guard holds.

Formal statement
import Definitions.Def_CookLevin_Basic

open CookLevin

theorem relocate_nextstate
    {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).1 = (cmd (gs.take k1)).1 := by sorry

View graph