A conditional assembled from supplied machine witnesses

This is the machine-witness portion of the existing conditional computability proof. Its constant absorbs the finite Boolean code and machine overhead; time and workspace remain independent.

theorem Turing.MultiTapeTM.Internal.conditional {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} {tc sc tf sf tg sg : α → ℕ} {kc kf kg : ℕ} {Qc Qf Qg : Type} [Finite Qc] [Finite Qf] [Finite Qg] {tmc : MultiTapeTM kc Bool Qc} {tmf : MultiTapeTM kf Bool Qf} {tmg : MultiTapeTM kg Bool Qg} (hc : ∀ (a : α), tmc.ComputesTidilyInTimeAndSpace (encIn a) (encC (c a)) (tc a) (sc a)) (hf : ∀ (a : { a : α // c a = true }), tmf.ComputesTidilyInTimeAndSpace (encIn ↑a) (encOut (f ↑a)) (tf ↑a) (sf ↑a)) (hg : ∀ (a : { a : α // c a = false }), tmg.ComputesTidilyInTimeAndSpace (encIn ↑a) (encOut (g ↑a)) (tg ↑a) (sg ↑a)) : ∃ (C : ℕ) (k : ℕ) (Q : Type) (_ : Finite Q) (tm : MultiTapeTM k Bool Q), ∀ (a : α), tm.ComputesTidilyInTimeAndSpace (encIn a) (encOut (if c a = true then f a else g a)) ((tc a + if c a = true then tf a else tg a) + C) ((sc a + if c a = true then sf a else sg a) + C)

Assemble the existing test/composition/conditional machines at independent branch bounds.