Prove2Me

Relocating a Turing machine to more tapes preserves well-formedness

Proved
machine_relocate_prefix_wf

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

Given a well-formed k1-tape Turing machine, there exists a well-formed k-tape machine (for k ≥ k1) that simulates it on the first k1 tapes. The construction relocates each command to act on the prefix tapes while leaving suffix tapes unchanged.

Formal statement
import Definitions.Def_CookLevin_Basic

open CookLevin

theorem machine_relocate_prefix_wf {k1 k G1 : Nat} {M1 : Machine}
    (hk : k1 ≤ k)
    (hwf : TuringMachine k1 G1 M1) :
    ∃ M : Machine, TuringMachine k G1 M := by sorry

View graph