nat_iterate — Mathlib

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']

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