Tidy computations as runs

A tidy computation (Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace) is the run of exactly the given number of steps from the start with blank work tapes to the halted configuration with blank work tapes that has emitted the output, together with the space bound. This is Turing.MultiTapeTM.computesTidily_iff as stated in Christian Reitwiessner's branch crei/tidy-universal, from which the vendored modules use it.

Main results

• Turing.MultiTapeTM.computesTidily_iff_runFrom: a tidy computation, read on runs.

theorem Turing.MultiTapeTM.computesTidily_iff_runFrom {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {input output : List Symbol} : tm.ComputesTidilyInTimeAndSpace input output t s ↔ runFrom (wordsCfg input (some tm.q₀) (fun (x : Fin k) => []) []) t = wordsCfg input none (fun (x : Fin k) => []) output ∧ space (wordsCfg input (some tm.q₀) (fun (x : Fin k) => []) []) t ≤ s

A tidy computation is a single run between Turing.wordsCfg configurations with blank work tapes, which emits the output, together with the space bound.