English
For all α, β, σ with Primcodable instances and any f: α → β → Option σ, the primrec-2 predicate of the function a ↦ decode β n bound to f a is equivalent to Primrec₂ f. More precisely, (Primrec₂ (λ a n, decode β n .bind (f a))) ⇔ Primrec₂ f.
Русский
Для всех типов α, β, σ с примкодируемыми инстанциями и любого функции f: α → β → Option σ верна равносильность: Primrec₂ (λ a n, decode β n .bind (f a)) ⇔ Primrec₂ f.
LaTeX
$$$\\operatorname{Primrec}_2\\bigl(\\lambda a\\, n. (\\operatorname{decode}\\ \\beta\\ n)\\,\\bind\\ (f\\ a)\\bigr) \\;\\Longleftrightarrow\\; \\operatorname{Primrec}_2 f.$$$
Lean4
theorem bind_decode_iff {f : α → β → Option σ} : (Primrec₂ fun a n => (@decode β _ n).bind (f a)) ↔ Primrec₂ f :=
⟨fun h => by simpa [encodek] using h.comp fst ((@Primrec.encode β _).comp snd), fun h =>
option_bind (Primrec.decode.comp snd) <| h.comp (fst.comp fst) snd⟩
