English
Let f be a Primrec' function of m arguments and let g be a vector-valued Primrec' function of n inputs. Then the composition v ↦ f(g(v)) is Primrec'.
Русский
Пусть f — примитивно-рекурсивная функция одной арности m и пусть g — векторно-значная примитивно-рекурсивная функция от n входов; тогда композиция v ↦ f(g(v)) является Primrec'.
LaTeX
$$$\forall {n,m} {f : List.Vector\ NAT\ m \to\ NAT} {g : List.Vector\ NAT\ n \to\ List.Vector\ NAT\ m},\ \mathrm{Primrec}'\ f \ \to\ \mathrm{Vec}\ n\ m\ g \ \to\ \mathrm{Primrec}'\ (fun\ v \to\ f (g\ v))$$$
Lean4
theorem comp' {n m f g} (hf : @Primrec' m f) (hg : @Vec n m g) : Primrec' fun v => f (g v) :=
(hf.comp _ hg).of_eq fun v => by simp
