CookLevin.turingCommand_relocate_prefix

import Definitions.Def_CookLevin_Basic

open CookLevin

/-- Prefix relocation of a command: run a `k1`-tape command on the first `k1`
    of `k` tapes, leaving the remaining tapes untouched (no-op actions).
    The guard ensures the alphabet bound is respected even on unreachable
    configurations; on reachable ones (symbols `< G1`) it always holds. -/
def relocatePrefixCmd (k1 k G1 : Nat) (cmd : Command) : Command :=
  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)))

theorem CookLevin.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 (relocatePrefixCmd k1 k G1 cmd) := by sorry