English
If f, g are computable and h is a computable 2-ary operation, then the function a ↦ Nat.rec (g a) (λ y IH. h a (y, IH)) (f a) is computable.
Русский
Если f, g вычислимы, а h — вычислимая бинарная операция, то функция a ↦ Nat.rec (g a) (λ y IH. h a (y, IH)) (f a) вычислима.
LaTeX
$$$\mathrm{Computable}\; f \land \mathrm{Computable}\; g \land \mathrm{Computable}_2\; h \Rightarrow \mathrm{Computable}\; (a \mapsto \mathrm{Nat}.rec (\mathrm{g}(a)) (\lambda y IH. h(a,(y,IH))) (f(a)))$$$
Lean4
theorem nat_rec {f : α → ℕ} {g : α → σ} {h : α → ℕ × σ → σ} (hf : Computable f) (hg : Computable g)
(hh : Computable₂ h) : Computable fun a => Nat.rec (motive := fun _ => σ) (g a) (fun y IH => h a (y, IH)) (f a) :=
(Partrec.nat_rec hf hg hh.partrec₂).of_eq fun a => by simp; induction f a <;> simp [*]
