Encoded function witnesses run on selected work tapes

These three generic machine lemmas are moved unchanged from Encodings.StepMachine. Their statements concern machine-level tidiness, not an asymptotic computability calculus.

theorem Turing.MultiTapeTM.transformsTapes_outputToWord {β : Type u_1} {δ : Type u_2} {k K : ℕ} {S : Type u_3} {tm : MultiTapeTM k Bool S} {encB : β ↪ List Bool} {encD : δ ↪ List Bool} {f : β → δ} {t s : β → ℕ} (h : tm.ComputesFunTidilyInTimeAndSpace encB encD f t s) {e : Fin (k + 1) ↪ Fin K} {V : Fin K} (he : e (Fin.last k) = V) (b : β) : (tm.outputToWord.extendTapes e).TransformsTapes (fun (inp : List Bool) (ws : Fin K → List Bool) => inp = encB b ∧ ws = fun (x : Fin K) => []) (fun (x : List Bool) (x_1 ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update (fun (x : Fin K) => []) V (encD (f b)) ∧ em = []) (t b + (encD (f b)).length + 2) (s b + 2 * (encD (f b)).length + 2 * K + 3)

A tidy machine writing its output to tape V.

theorem Turing.MultiTapeTM.transformsTapes_inputFromWord_fun {β : Type u_1} {δ : Type u_2} {k K : ℕ} {S : Type u_3} {tm : MultiTapeTM k Bool S} {encB : β ↪ List Bool} {encD : δ ↪ List Bool} {f : β → δ} {t s : β → ℕ} (h : tm.ComputesFunTidilyInTimeAndSpace encB encD f t s) {e : Fin (k + 2) ↪ Fin K} {V : Fin K} (he : e (Fin.natAdd k 0) = V) (b : β) : ((tm.inputFromWord true).extendTapes e).TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (encB b)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = ws ∧ em = encD (f b)) (t b + 4) (s b + 2 * (encB b).length + 3 * K + 10)

A tidy machine run on the word on tape V, emitting its output.

theorem Turing.MultiTapeTM.transformsTapes_onWords {β : Type u_1} {δ : Type u_2} {k K : ℕ} {S : Type u_3} {tm : MultiTapeTM k Bool S} {encB : β ↪ List Bool} {encD : δ ↪ List Bool} {f : β → δ} {t s : β → ℕ} (h : tm.ComputesFunTidilyInTimeAndSpace encB encD f t s) {e : Fin (k + 1 + 2) ↪ Fin K} {V O : Fin K} (hi : e (Fin.natAdd (k + 1) 0) = V) (ho : e (Fin.castAdd 2 (Fin.last k)) = O) (b : β) : ((tm.onWords true).extendTapes e).TransformsTapes (fun (x : List Bool) (ws : Fin K → List Bool) => ws = Function.update (fun (x : Fin K) => []) V (encB b)) (fun (x : List Bool) (ws ws' : Fin K → List Bool) (em : List Bool) => ws' = Function.update ws O (encD (f b)) ∧ em = []) (t b + (encD (f b)).length + 6) (s b + 2 * (encB b).length + 2 * (encD (f b)).length + 4 * K + 15)

A tidy machine run on the word on tape V, writing its output to tape O.