The existing concatenation machine and its run theorem

Machine declarations are moved from their original module without changing programs or resource formulas. Higher computability-calculus theorems remain in the original facade.

noncomputable def Turing.MultiTapeTM.appendTM {k₁ k₂ : ℕ} {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (tm₁ : MultiTapeTM k₁ Symbol S₁) (tm₂ : MultiTapeTM k₂ Symbol S₂) : MultiTapeTM (max k₁ k₂) Symbol (S₁ ⊕ S₂)

Run tm₁ and then tm₂, both with their work tapes padded to max k₁ k₂.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.append {k₁ k₂ : ℕ} {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} {tm₁ : MultiTapeTM k₁ Symbol S₁} {tm₂ : MultiTapeTM k₂ Symbol S₂} {x y₁ y₂ : List Symbol} {t₁ s₁ t₂ s₂ : ℕ} (h₁ : tm₁.ComputesTidilyInTimeAndSpace x y₁ t₁ s₁) (h₂ : tm₂.ComputesTidilyInTimeAndSpace x y₂ t₂ s₂) : (tm₁.appendTM tm₂).ComputesTidilyInTimeAndSpace x (y₁ ++ y₂) (t₁ + t₂) (s₁ + s₂ + 2 * max k₁ k₂)

If tm₁ computes y₁ from x tidily and tm₂ computes y₂ from x tidily, then appendTM tm₁ tm₂ computes y₁ ++ y₂ from x tidily.