The space of the work-tape-rewinding machine

The addition of Christian Reitwiessner's branch crei/tidy-universal to Cslib.Computability.Machines.Turing.MultiTape.Plumbing.RewindWork.

Main results

• Turing.MultiTapeTM.space_rewindWork_le: the rewinding machine visits at most p + 2 cells.

theorem Turing.MultiTapeTM.space_rewindWork_le {Symbol : Type u_1} {input : List Symbol} (write : Option (Option Symbol)) (ip : Fin (input.length + 2)) (t : ℤ → Option Symbol) (out : List Symbol) {w : List Symbol} (hw : t = tapeOfList w) {p : ℕ} (hp : p ≤ w.length) (n : ℕ) : space { state := some (rewindWork Symbol write).q₀, inputPos := ip, workTapes := fun (x : Fin 1) => t, workTapePos := fun (x : Fin 1) => ↑p, output := out } n ≤ p + 2

The one-tape rewindWork machine visits at most p + 2 cells: its head stays within [-1, p].