English
For any f: α → β → σ with primcodable α, β, σ, encoding the outputs of f preserves primitive recursiveness: Primrec₂ (a,b) ↦ encode(f(a,b)) iff Primrec₂ f.
Русский
Для любых f: α → β → σ с примитивно кодируемыми α, β, σ сохранение кодирования выходов f сохраняет примитивную рекурсию: Primrec₂ (a,b) ↦ encode(f(a,b)) эквивалентно Primrec₂ f.
LaTeX
$$$\bigl(\operatorname{Primrec}_2\, (\lambda a,b. \operatorname{encode}(f(a,b)))\bigr) \iff \operatorname{Primrec}_2 f$$$
Lean4
theorem encode_iff {f : α → β → σ} : (Primrec₂ fun a b => encode (f a b)) ↔ Primrec₂ f :=
Primrec.encode_iff