Head movement along run paths

This file collects how a step moves the work-tape heads and changes the work tapes, and what this implies for the cells visited along a run path: a head moves by at most one cell per step, so it visits every cell between its first and last positions, and a cell changes only under its head.

theorem Turing.MultiTapeNTM.Step.workTapePos_le {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (i : Fin k) : |c'.workTapePos i - c.workTapePos i| ≤ 1

A work-tape head moves by at most one cell in a single step.

theorem Turing.MultiTapeNTM.Step.workTapes_eq_of_ne {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {c c' : Cfg k Symbol State input} (h : ntm.Step c c') {i : Fin k} {z : ℤ} (hz : z ≠ c.workTapePos i) : c'.workTapes i z = c.workTapes i z

A step does not change a work-tape cell away from its head.

theorem Turing.MultiTapeNTM.RunPath.uIcc_workTapePos_subset_visitedByTapeHead {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) (i : Fin k) : Finset.uIcc ((RelSeries.head p).workTapePos i) ((RelSeries.last p).workTapePos i) ⊆ p.visitedByTapeHead i

Every position between the first and the last position of a head along a path is visited, since the head moves by at most one cell per step.

theorem Turing.MultiTapeNTM.RunPath.mem_visitedByTapeHead_of_workTapes_ne {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) {i : Fin k} {z : ℤ} (h : (RelSeries.last p).workTapes i z ≠ (RelSeries.head p).workTapes i z) : z ∈ p.visitedByTapeHead i

A work-tape cell that differs between the first and the last configuration of a path was visited by its head.

theorem Turing.MultiTapeNTM.RunPath.natAbs_le_spaceUsedByTape_of_mem_visited {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) {i : Fin k} {z : ℤ} (hz : z ∈ p.visitedByTapeHead i) : (z - (RelSeries.head p).workTapePos i).natAbs ≤ p.spaceUsedByTape i

Every position visited by a head lies within the space of its tape from its first position.

theorem Turing.MultiTapeNTM.RunPath.inWindow_of_space_le {k : ℕ} {State : Type u_1} {Symbol : Type u_3} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {p : ntm.RunPath input} {s : ℕ} (h0 : ∀ (i : Fin k), (RelSeries.head p).workTapePos i = 0) (hs : p.space ≤ s) : p.InWindow s

A path that starts with every head at cell 0 and visits at most s cells keeps its heads within [-s, s].