Rewinding a list of tapes, one at a time

Rewinding cannot be done in one uniform pass the way wiping can: TM.rewindWorkTM bounces at ▷ rather than saturating there, so moving everyone left the same number of times oscillates. Doing it one tape at a time via TM.bigSeqTM works once every tape has been parked once (TM.parkAll_hoareTime).

Main results

• TM.rewindList_hoareTime — rewind every targeted tape to cell 1

theorem Complexity.TM.rewindList_hoareTime {n : ℕ} (targets : List (Fin n)) : targets.Nodup → ∀ (B : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape), Parked inp₀ → Parked out₀ → (∀ (j : Fin n), Parked (work₀ j)) → (∀ j ∈ targets, (work₀ j).cells 0 = Γ.start ∧ (work₀ j).head ≤ B) → (bigSeqTM (List.map rewindWorkTM targets)).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 = inp₀ ∧ out = out₀ ∧ (∀ j ∈ targets, work j = { head := 1, cells := (work₀ j).cells }) ∧ ∀ j ∉ targets, work j = work₀ j) (targets.length * (B + 3) + 1)

Rewinding a list of tapes, one at a time. Given a uniform head bound B and that every tape (not just the targets) is already Parked — the state after parkAll_hoareTime — sequentially rewinding each named tape lands it at cell 1 with its cells unchanged, leaving every other tape (targeted-but-not-yet-reached, or never targeted) exactly as it was.