English
If f is a binary Primrec' function with appropriate coordinate extraction, and g,h are Primrec' on n inputs, then the two-argument composition v ↦ f (g v) (h v) is Primrec'.
Русский
Если f — бинарная примитивно-рекурсивная функция и g,h — примитивно-рекурсивные функции от одних входов, то композиция v ↦ f (g v) (h v) также примитивно-рекурсивна.
LaTeX
$$$\forall f:\ NAT\to\ NAT\to\ NAT,\ hf:\ Primrec'\ 2\ (\lambda v. f\ v.head\ v.tail.head),\ \forall {n}\ {g}\ {h}:\ List.Vector\ NAT\ n \to\ NAT,\ hg:\ Primrec'\ n\ g,\ hh:\ Primrec'\ n\ h\Rightarrow\ Primrec'\ (fun\ v\to\ f (g\ v) (h\ v)).$$$
Lean4
theorem comp₂ (f : ℕ → ℕ → ℕ) (hf : @Primrec' 2 fun v => f v.head v.tail.head) {n g h} (hg : @Primrec' n g)
(hh : @Primrec' n h) : Primrec' fun v => f (g v) (h v) := by simpa using hf.comp' (hg.cons <| hh.cons Primrec'.nil)
