English
If o : α → Option β is Primrec, f : α → σ is Primrec, and g : α → β → σ is Primrec₂, then the function a ↦ Option.casesOn (o a) (f a) (g a) is Primrec.
Русский
Если o : α → Option β примитивно рекурсивна, f : α → σ — Primrec, g : α → β → σ — Primrec₂, то функция a ↦ Option.casesOn (o a) (f a) (g a) является Primrec.
LaTeX
$$$ Primrec o \rightarrow Primrec f \rightarrow Primrec_2 g \rightarrow Primrec (\\lambda a. Option.casesOn (o a) (f a) (g a))$$$
Lean4
theorem option_casesOn {o : α → Option β} {f : α → σ} {g : α → β → σ} (ho : Primrec o) (hf : Primrec f)
(hg : Primrec₂ g) : @Primrec _ σ _ _ fun a => Option.casesOn (o a) (f a) (g a) :=
encode_iff.1 <|
(nat_casesOn (encode_iff.2 ho) (encode_iff.2 hf) <|
pred.comp₂ <|
Primrec₂.encode_iff.2 <|
(Primrec₂.nat_iff'.1 hg).comp₂ ((@Primrec.encode α _).comp fst).to₂ Primrec₂.right).of_eq
fun a => by rcases o a with - | b <;> simp [encodek]
