prim_iff₂ — Mathlib

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)⟩

Похожие утверждения