Suffix-relocated Turing command preserves command well-formedness

Proved

turingCommand_relocate_suffix

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

A k1-tape Turing command relocated to tapes off..off+k1-1 of a k-tape machine (leaving other tapes untouched) is a well-formed k-tape Turing command.

Formal statement

import Definitions.Def_CookLevin_Basic

open CookLevin

theorem turingCommand_relocate_suffix
    {off k1 k Q1 Q G1 G : Nat} {cmd : Command}
    (hk1 : 0 < k1) (hoff : off + k1 ≤ k) (hQ : Q1 ≤ Q) (hG : G1 ≤ G)
    (hcmd : TuringCommand k1 Q1 G1 cmd) :
    TuringCommand k Q G (fun gs =>
      if _h : ∀ i < k1, ((gs.drop off).take k1)[i]! < G1 then
        ((cmd ((gs.drop off).take k1)).1,
         (List.range off).map (fun j => (gs[j]!, Direction.Stay)) ++
         (cmd ((gs.drop off).take k1)).2 ++
         (List.range (k - off - k1)).map (fun j => (gs[off + k1 + j]!, Direction.Stay)))
      else
        (0, gs.map (fun s => (s, Direction.Stay)))) := by sorry

View graph