Confined runs

The addition of Christian Reitwiessner's branch crei/tidy-universal to Cslib.Computability.Machines.Turing.MultiTape.Plumbing.RepeatUntilBlank: a run between two configurations that keeps every head within a window, which loops built like Turing.MultiTapeTM.repeatUntilBlank accumulate round by round. The branch also reproves Turing.MultiTapeTM.transformsTapes_repeatUntilBlank through confined runs; that proof is not copied.

Main definitions

• Turing.MultiTapeTM.ConfinedRun: a run of a given length, with every head within [-r, r].

structure Turing.MultiTapeTM.ConfinedRun {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (M : MultiTapeTM k Symbol State) (start finish : Cfg k Symbol State input) (steps r : ℕ) : Prop

M runs from start to finish in steps steps, with every head within [-r, r].

• reaches : runFrom start steps = finish
• confined (l : Fin k) : visitedByTapeHead start steps l ⊆ Finset.Icc (-↑r) ↑r