English
Two-argument partial functions compose naturally: if f is Partrec₂, and g,h computable, then the function a,b ↦ f (g a b) (h a b) is Partrec₂.
Русский
Двухарные частичные функции естественным образом компонуются: если f частично-двухарная, а g,h вычислимы, то a,b ↦ f (g a b) (h a b) частично рекурсивна.
LaTeX
$$$\forall f:\gamma\to^.\delta,\forall g:\alpha\to\beta,\forall h:\alpha\to\beta,\ Partrec_2(f) \rightarrow Computable_2(g) \rightarrow Computable_2(h) \\Rightarrow Partrec_2(\lambda a,b. f(g(a,b), h(a,b))).$$
Lean4
theorem comp₂ {f : γ → δ →. σ} {g : α → β → γ} {h : α → β → δ} (hf : Partrec₂ f) (hg : Computable₂ g)
(hh : Computable₂ h) : Partrec₂ fun a b => f (g a b) (h a b) :=
hf.comp hg hh
