English
A two-argument Primrec' function is primitive recursive, and conversely.
Русский
Функция арности 2 Primrec' эквивалентна Primrec.
LaTeX
$$$\forall {f : NAT \to NAT \to NAT},\ (@Primrec'\ 2 fun v => f v.head v.tail.head) \leftrightarrow \ Primrec\ f$$$
Lean4
theorem prim_iff₂ {f : ℕ → ℕ → ℕ} : (@Primrec' 2 fun v => f v.head v.tail.head) ↔ Primrec₂ f :=
prim_iff.trans
⟨fun h =>
(h.comp <| Primrec.vector_cons.comp .fst <| Primrec.vector_cons.comp .snd (.const nil)).of_eq fun v => by simp,
fun h => h.comp .vector_head (Primrec.vector_head.comp .vector_tail)⟩