comp₂ — Mathlib

English

If f is Primrec₂ and g,h are Primrec, then the composition a ↦ f(g(a), h(a)) is Primrec₂.

Русский

Если f является Primrec₂, а g и h примитивно вычислимые, то композиция a ↦ f(g(a), h(a)) является Primrec₂.

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 : α → β → γ} (hf : Primrec f) (hg : Primrec₂ g) : Primrec₂ fun a b => f (g a b) :=
  hf.comp hg

Похожие утверждения