English
If f,g,h are Primrec in the respective senses, then the function a ↦ Nat.rec (g a) (λ n IH. h a (n, IH)) (f a) is Primrec.
Русский
Если f,g,h примитивно рекурсивны в соответствующих смыслах, то функция a ↦ Nat.rec (g a) (λ n IH. h a (n, IH)) (f a) является Primrec.
LaTeX
$$$ Primrec f \rightarrow Primrec g \rightarrow Primrec_2 h \rightarrow Primrec (\\lambda a. (f a).rec (motive := (\\lambda _ => β)) (g a) (\\lambda n IH. h a (n, IH)))$$$
Lean4
theorem nat_rec' {f : α → ℕ} {g : α → β} {h : α → ℕ × β → β} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) :
Primrec fun a => (f a).rec (motive := fun _ => β) (g a) fun n IH => h a (n, IH) :=
(nat_rec hg hh).comp .id hf
