Legacy existential work-tape interface

The existing machine and fixed-machine run laws are reexported from the Internal kernel.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.exists_onWords {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s : α → ℕ} (h : ComputableTidilyInTimeAndSpace f encIn encOut t s) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM (k + 1 + 2) Bool State) (i : Fin (k + 1 + 2)) (o : Fin (k + 1 + 2)), i ≠ o ∧ ∀ (a : α), tm.TransformsTapes (fun (x : List Bool) (ws : Fin (k + 1 + 2) → List Bool) => ws = Function.update (fun (x : Fin (k + 1 + 2)) => []) i (encIn a)) (fun (x : List Bool) (ws ws' : Fin (k + 1 + 2) → List Bool) (emitted : List Bool) => ws' = Function.update ws o (encOut (f a)) ∧ emitted = []) (t a + (encOut (f a)).length + 6) (s a + 2 * (encIn a).length + 2 * (encOut (f a)).length + 3 * k + 18)

A tidily computable function is computed by a machine with binary alphabet and finitely many states that reads its input from a work tape i and writes its output to a different work tape o, leaving every other work tape unchanged and emitting nothing.