Parking every tape at once

Rewinding tapes one at a time needs every tape not being rewound to be Parked already — a tape still reading ▷ would bounce to cell 1 as a side effect. One TM.skipTM step with no target achieves that uniformly: from Tape.StartInvariant alone, cell-0 tapes bounce to cell 1 and parked tapes stay put.

Main results

• TM.parkAll_hoareTime — one step parks every tape

theorem Complexity.TM.move_idleDir_eq_of_startInvariant {t : Tape} (h : t.StartInvariant) : t.move (idleDir t.read) = { head := max t.head 1, cells := t.cells }

One idle step on a StartInvariant tape is exactly a bounce off ▷ if it was there, and otherwise a no-op: the resulting head is max t.head 1.

theorem Complexity.TM.parked_move_idleDir_of_startInvariant {t : Tape} (h : t.StartInvariant) : Parked (t.move (idleDir t.read)) ∧ (t.move (idleDir t.read)).cells = t.cells

One idle step parks a StartInvariant tape: bounces it off ▷ if it was there, and otherwise leaves it exactly as it was.

theorem Complexity.TM.parkAll_hoareTime {n : ℕ} (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinp : inp₀.StartInvariant) (hwork : ∀ (i : Fin n), (work₀ i).StartInvariant) (hout : out₀.StartInvariant) : skipTM.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = { head := max inp₀.head 1, cells := inp₀.cells } ∧ (∀ (i : Fin n), work i = { head := max (work₀ i).head 1, cells := (work₀ i).cells }) ∧ out = { head := max out₀.head 1, cells := out₀.cells }) 1

Parking every tape at once. From tapes satisfying only StartInvariant, one skipTM step brings every one of them to Parked, preserving all cell contents exactly.