The existing composition 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.comp {k₁ k₂ : ℕ} {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (tm₂ : MultiTapeTM k₂ Symbol S₂) (tm₁ : MultiTapeTM k₁ Symbol S₁) (mark : Symbol) : MultiTapeTM (max k₁ k₂ + 2) Symbol ((S₁ ⊕ RewindWorkState) ⊕ (MarkWorkState ⊕ S₂ ⊕ MarkWorkState) ⊕ Unit ⊕ RewindWorkState)

tm₂ after tm₁, both with their work tapes padded to max k₁ k₂: run tm₁ with its output written to the work tape Fin.natAdd (max k₁ k₂) 0, run tm₂ reading its input from that tape (using mark on the last work tape to flag the left end of the input), then clear that tape.

theorem Turing.MultiTapeTM.transformsTapes_clearWork_only {Symbol : Type u_1} {k : ℕ} (i : Fin k) (w : List Symbol) : ((clearWork Symbol).extendTapes (tapeEmb i)).TransformsTapes (fun (x : List Symbol) (ws : Fin k → List Symbol) => ws = Function.update (fun (x : Fin k) => []) i w) (fun (x : List Symbol) (x_1 ws' : Fin k → List Symbol) (e : List Symbol) => (ws' = fun (x : Fin k) => []) ∧ e = []) (3 * (w.length + 1)) (w.length + 1 + k)

Clearing the only non-blank work tape leaves all work tapes blank.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.comp {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 w y : List Symbol} {t₁ s₁ t₂ s₂ : ℕ} (h₁ : tm₁.ComputesTidilyInTimeAndSpace x w t₁ s₁) (h₂ : tm₂.ComputesTidilyInTimeAndSpace w y t₂ s₂) (mark : Symbol) : (tm₂.comp tm₁ mark).ComputesTidilyInTimeAndSpace x y (t₁ + t₂ + 4 * w.length + 9) (s₁ + s₂ + 5 * w.length + (6 * max k₁ k₂ + 20))

If tm₁ computes w from x tidily and tm₂ computes y from w tidily, then tm₂.comp tm₁ mark computes y from x tidily.