Legacy fold certificate facade

The machine construction lives in the Internal fold compiler. This compatibility theorem retains its original statement for callers still using the staged existential tidy interface.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.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 : γ → ℕ} (hlist : ComputableTidilyInTimeAndSpace list encIn encL t s) (hinit : ComputableTidilyInTimeAndSpace init encIn encB t s) (hstep : ComputableTidilyInTimeAndSpace (fun (p : β × α) => step p.1 p.2) encBA encB tStep sStep) (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 : ℕ), ComputableTidilyInTimeAndSpace (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB (fun (x : γ) => c * (t x + ((list x).length + 1) * (tMax x + lMax x + 1))) fun (x : γ) => c * (s x + sMax x + lMax x + 1)