The existing fold compiler from supplied machine witnesses

theorem Turing.MultiTapeTM.Internal.FoldCompiler.foldl {γ α β : Type u} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encBA : β × α ↪ List Bool} {encS : List α × β ↪ List Bool} {encO : Option (List α × β) ↪ List Bool} [hLE : ListEncoding encA encL] [hBA : PairEncoding encB encA encBA] [hSE : PairEncoding encL encB encS] [hOE : OptionEncoding encS encO] {list : γ → List α} {init : γ → β} {step : β → α → β} {t s : γ → ℕ} {tStep sStep : β × α → ℕ} {tMax sMax lMax : γ → ℕ} {kl ki ks : ℕ} {Ql Qi Qs : Type} [Finite Ql] [Finite Qi] [Finite Qs] {tml : MultiTapeTM kl Bool Ql} {tmi : MultiTapeTM ki Bool Qi} {tms : MultiTapeTM ks Bool Qs} (hlist : ∀ (x : γ), tml.ComputesTidilyInTimeAndSpace (encIn x) (encL (list x)) (t x) (s x)) (hinit : ∀ (x : γ), tmi.ComputesTidilyInTimeAndSpace (encIn x) (encB (init x)) (t x) (s x)) (hstep : ∀ (p : β × α), tms.ComputesTidilyInTimeAndSpace (encBA p) (encB (step p.1 p.2)) (tStep p) (sStep p)) (htMax : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), tStep (List.foldl step (init x) (List.take i (list x)), (list x)[i]) ≤ tMax x) (hsMax : ∀ (x : γ) (i : ℕ) (hi : i < (list x).length), sStep (List.foldl step (init x) (List.take i (list x)), (list x)[i]) ≤ sMax x) (hlMax : ∀ (x : γ), ∀ i ≤ (list x).length, (encS (List.drop i (list x), List.foldl step (init x) (List.take i (list x)))).length ≤ lMax x) : ∃ (c : ℕ) (k : ℕ) (Q : Type) (_ : Finite Q) (tm : MultiTapeTM k Bool Q), ∀ (x : γ), tm.ComputesTidilyInTimeAndSpace (encIn x) (encB (List.foldl step (init x) (list x))) (c * (t x + ((list x).length + 1) * (tMax x + lMax x + 1))) (c * (s x + sMax x + lMax x + 1))

Compile a fold from supplied machines, with the original independent prefix bounds.