English
If f,g,h are Primrec as specified, then a ↦ (h a)^[f a] (g a) is Primrec.
Русский
Если f,g,h примитивно рекурсивны, то функция a ↦ (h a)^[f a] (g a) является Primrec.
LaTeX
$$$ Primrec f \rightarrow Primrec g \rightarrow Primrec_2 h \rightarrow Primrec (\\lambda a. (h a)^[f a] (g a))$$$
Lean4
theorem nat_iterate {f : α → ℕ} {g : α → β} {h : α → β → β} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ h) :
Primrec fun a => (h a)^[f a] (g a) :=
(nat_rec' hf hg (hh.comp₂ Primrec₂.left <| snd.comp₂ Primrec₂.right)).of_eq fun a => by
induction f a <;> simp [*, -Function.iterate_succ, Function.iterate_succ']