Prefix-relocated Turing command preserves command well-formedness

Proved

turingCommand_relocate_prefix

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

Prefix relocation of a Turing command (running a k1-tape command on the first k1 of k tapes, with no-ops on the rest) preserves the TuringCommand well-formedness property, provided the tape/state/alphabet bounds are monotone.

Formal statement

import Definitions.Def_CookLevin_Basic

open CookLevin

theorem turingCommand_relocate_prefix
    {k1 k Q1 Q G1 G : Nat} {cmd : Command}
    (hk : k1 ≤ k) (hQ : Q1 ≤ Q) (hG : G1 ≤ G) (hk1 : 0 < k1)
    (hcmd : TuringCommand k1 Q1 G1 cmd) :
    TuringCommand k Q G (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)))) := by sorry

View graph