Output growth along run paths

The additions of cslib PR #1111 to Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic: a step emits at most one symbol, so a run path emits at most one symbol per step.

Main results

• Turing.MultiTapeNTM.RunPath.length_output_last_le: a run path emits at most one symbol per step.

theorem Turing.MultiTapeNTM.RunPath.length_output_le_of_step {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} {c c' : Cfg k Symbol State input} (h : ntm.Step c c') : c'.output.length ≤ c.output.length + 1

A step emits at most one symbol.

theorem Turing.MultiTapeNTM.RunPath.length_output_last_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {ntm : MultiTapeNTM k Symbol State} (p : ntm.RunPath input) : (RelSeries.last p).output.length ≤ (RelSeries.head p).output.length + p.time

A run path emits at most one symbol per step.