English
If f, g are primitive recursive and h is a primitive recursive binary function, then the function a ↦ (f(a)).foldl (λ s b, h(a,(s,b))) (g(a)) is primitive recursive.
Русский
Если f, g примитивно вычислимы, а h — примитивно вычислимая бинарная функция, то функция a ↦ (f(a)).foldl (λ s b, h(a,(s,b))) (g(a)) является примитивно вычислимой.
LaTeX
$$$\\mathrm{Primrec}\,f \\to \\mathrm{Primrec}\,g \\to \\mathrm{Primrec}_2\\,h \\to \\mathrm{Primrec}\\left( a \\mapsto (f(a)).\\mathrm{foldl}\\left( \\lambda s,b. h\\left(a,(s,b)\\right) \\right)\\left(g(a)\\right) \\right)$$$
Lean4
theorem list_foldl {f : α → List β} {g : α → σ} {h : α → σ × β → σ} :
Primrec f → Primrec g → Primrec₂ h → Primrec fun a => (f a).foldl (fun s b => h a (s, b)) (g a) :=
list_foldl' (Primcodable.prim _)
