Basic semantic facts for tidy machine runs #
Machine declarations are moved from their original module without changing programs or resource formulas. Higher computability-calculus theorems remain in the original facade.
theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.computesInTimeAndSpace {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {input output : List Symbol} (h : tm.ComputesTidilyInTimeAndSpace input output t s) :
tm.ComputesInTimeAndSpace input output t s
A tidy computation is a computation in the sense of
Turing.MultiTapeTM.ComputesInTimeAndSpace.
theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.length_output_le {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {input output : List Symbol} (h : tm.ComputesTidilyInTimeAndSpace input output t s) :
A tidy computation within t steps emits at most t symbols.
theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.extendTapes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {input output : List Symbol} {k' : ℕ} (h : tm.ComputesTidilyInTimeAndSpace input output t s) (e : Fin k ↪ Fin k') :
(tm.extendTapes e).ComputesTidilyInTimeAndSpace input output t (s + (k' - k))
A tidy computation stays tidy with more work tapes, at one cell per added tape.