English
If f is Primrec' on one argument via the head of its input, and g is Primrec' on n inputs, then the composition v ↦ f (g v) is Primrec'.
Русский
Если f — примитивно-рекурсивная функция одного аргумента, получаемая через первый элемент входа, и g — примитивно-рекурсивная функция от n входов, то композиция v ↦ f (g v) также примитивно-рекурсивна.
LaTeX
$$$\forall f:\ NAT\to\NAT,\ hf:\ Primrec'\ 1\ (\lambda v. f\ v.head),\ \forall n\ g:\ List.Vector\ NAT\ n \to\ NAT,\ hg:\ Primrec'\ n\ g\Rightarrow\ Primrec'\ (fun\ v\to\ f (g\ v)).$$$
Lean4
theorem comp₁ (f : ℕ → ℕ) (hf : @Primrec' 1 fun v => f v.head) {n g} (hg : @Primrec' n g) : Primrec' fun v => f (g v) :=
hf.comp _ fun _ => hg
