English
Let f: α × β → σ. If there exist primitive recursive m, l and g with an order relation and a halting condition that reproduces f, then f is primitive recursive (as a two-argument function).
Русский
Пусть f: α × β → σ. Если существуют примитивно рекурсивные m, l, g, удовлетворяющие условию порядка и останова и восстанавливающие f, то f является примитивно-рекурсивной функцией (по двум аргументам).
LaTeX
$$$\mathrm{PR}_2(f) \leftarrow \text{if } m,l,g\text{ satisfy Primrec data and Ord, H, then } \mathrm{PR}_2(f).$$$
Lean4
theorem nat_omega_rec (f : α → β → σ) {m : α → β → ℕ} {l : α → β → List β} {g : α → β × List σ → Option σ}
(hm : Primrec₂ m) (hl : Primrec₂ l) (hg : Primrec₂ g) (Ord : ∀ a b, ∀ b' ∈ l a b, m a b' < m a b)
(H : ∀ a b, g a (b, (l a b).map (f a)) = some (f a b)) : Primrec₂ f :=
Primrec₂.uncurry.mp <|
nat_omega_rec' (Function.uncurry f) (Primrec₂.uncurry.mpr hm)
(list_map (hl.comp fst snd) (Primrec₂.pair.comp₂ (fst.comp₂ .left) .right))
(hg.comp₂ (fst.comp₂ .left) (Primrec₂.pair.comp₂ (snd.comp₂ .left) .right)) (by simpa using Ord)
(by simpa [Function.comp] using H)
