Runs of tidy computations

A tidy computation (Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace) is, in particular, a run from the initial configuration that has halted after the given number of steps with the given output.

Main results

• Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.runFrom_initCfg_eq.
• Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.runFrom_initCfg.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.runFrom_initCfg_eq {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {t s : ℕ} (h : tm.ComputesTidilyInTimeAndSpace input output t s) : runFrom (tm.initCfg input) t = wordsCfg input none (fun (x : Fin k) => []) output

A tidy computation restores all work tapes and heads within its stated time bound.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.runFrom_initCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {t s : ℕ} (h : tm.ComputesTidilyInTimeAndSpace input output t s) : (runFrom (tm.initCfg input) t).Halted ∧ (runFrom (tm.initCfg input) t).output = output

A tidy computation halts after the given number of steps from the initial configuration, with the given output.