English
If f is partial recursive and g is a two-argument partial recursive function, then the function a ↦ (f a).bind (g a) is partial recursive.
Русский
Если f частично рекурсивна и g — частично рекурсивная двоичная функция, то a ↦ (f a).bind (g a) частично рекурсивна.
LaTeX
$$$\forall f,g:\alpha\to^.\beta,\;\forall hf\ Partrec(f),\;\forall hg: Partrec_2(g)\;\Rightarrow\ Partrec(\lambda a. (f(a)).bind (g(a))).$$
Lean4
protected theorem bind {f : α →. β} {g : α → β →. σ} (hf : Partrec f) (hg : Partrec₂ g) :
Partrec fun a => (f a).bind (g a) :=
(hg.comp (Nat.Partrec.some.pair hf)).of_eq fun n => by simp [Seq.seq];
rcases e : decode (α := α) n with - | a <;> simp [e, encodek]
