English
Let R be a relation; if f and g are two-ary primitive recursive components, then the relation a,b ↦ R(f(a,b), g(a,b)) is primitive recursive in the Relational sense.
Русский
Пусть R — двоичное отношение; если f и g — примитивно вычислимые по двум аргументам, то отношение a,b ↦ R(f(a,b), g(a,b)) является примитивно вычислимым в реляционном смысле.
LaTeX
$$$\operatorname{PrimrecRel} R \to \operatorname{Primrec}_2 f \to \operatorname{Primrec}_2 g \to \operatorname{PrimrecRel}(a,b \mapsto R(f(a,b), g(a,b)))$$$
Lean4
theorem comp₂ {R : γ → δ → Prop} {f : α → β → γ} {g : α → β → δ} :
PrimrecRel R → Primrec₂ f → Primrec₂ g → PrimrecRel fun a b => R (f a b) (g a b) :=
PrimrecRel.comp
