Every work tape costs a cell

The additions of cslib PR #1138 to Cslib.Computability.Machines.Turing.MultiTape.Space: every work head visits the cell it starts on, so a run path visits at least one cell per work tape, and a space bound is at least the number of work tapes.

Main results

• Turing.MultiTapeNTM.RunPath.le_space: a run path visits at least k cells.
• Turing.MultiTapeNTM.RunsInSpace.le: a space bound is at least the number of work tapes.

theorem Turing.MultiTapeNTM.RunPath.le_space {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) : k ≤ p.space

Every work head visits at least the cell it starts on, so a path visits at least k cells.

theorem Turing.MultiTapeNTM.RunsInSpace.le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {s : ℕ} (h : ntm.RunsInSpace input s) : k ≤ s

A space bound leaves room for every work tape: already the computation path that has not moved yet visits one cell per tape.