English
A one-argument Primrec' function is primitive recursive, and conversely.
Русский
Функция единичной арности Primrec' эквивалентна Primrec.
LaTeX
$$$\forall {f : \mathbb{N} \to \mathbb{N}},\ (@Primrec'\ 1 \ fun v => f\ v.head) \leftrightarrow \ Primrec\ f$$$
Lean4
theorem prim_iff₁ {f : ℕ → ℕ} : (@Primrec' 1 fun v => f v.head) ↔ Primrec f :=
prim_iff.trans ⟨fun h => (h.comp <| .vector_ofFn fun _ => .id).of_eq fun v => by simp, fun h => h.comp .vector_head⟩