English
For every f : α → β → σ, Primrec₂ f holds if and only if a corresponding encoded one-argument natural-number function is Primrec.
Русский
Для всякой функции f : α → β → σ выполнено: Primrec₂ f эквивалентно тому, что соответствующая закодированная однозначная функция на натуральных числах Primrec.
LaTeX
$$$ Primrec_2 f \iff Nat.Primrec (Nat.unpaired (\lambda m n. encode (\{ decode\ α\ m \} .bind (\lambda a. \{ decode\ β\ n \} .map (f a)) )))$$$
Lean4
theorem nat_iff {f : α → β → σ} :
Primrec₂ f ↔ Nat.Primrec (.unpaired fun m n => encode <| (@decode α _ m).bind fun a => (@decode β _ n).map (f a)) :=
by
have :
∀ (a : Option α) (b : Option β),
Option.map (fun p : α × β => f p.1 p.2) (Option.bind a fun a : α => Option.map (Prod.mk a) b) =
Option.bind a fun a => Option.map (f a) b :=
fun a b => by cases a <;> cases b <;> rfl
simp [Primrec₂, Primrec, this]
