English
Let f be a two-argument primitive recursive function and g,h be primitive recursive unary functions. Then the two-argument function a,b ↦ f(g(a), h(a)) is primitive recursive in two arguments.
Русский
Пусть f — примитивно вычислимая функция двух аргументов, а g, h — примитивно вычислимые унарные функции. Тогда функция a,b ↦ f(g(a), h(a)) примитивно вычислима как функция двух переменных.
LaTeX
$$$\operatorname{Primrec}_2 f \to \operatorname{Primrec} g \to \operatorname{Primrec} h \to \operatorname{Primrec}_2 (a,b \mapsto f(g(a), h(a)))$$
Lean4
theorem comp {f : β → γ → σ} {g : α → β} {h : α → γ} (hf : Primrec₂ f) (hg : Primrec g) (hh : Primrec h) :
Primrec fun a => f (g a) (h a) :=
Primrec.comp hf (hg.pair hh)
