English
If o, f are computable and g is Partrec₂, then a ↦ Option.casesOn(o a) (f a) (g a) is computable.
Русский
Если o и f вычислимы, а g частично вычислима как двуарная операция, то функция a ↦ Option.casesOn (o a) (f a) (g a) вычислима.
LaTeX
$$$\mathrm{Computable}\; o \to \mathrm{Computable}\; f \to \mathrm{Partrec}_2\; g \Rightarrow \mathrm{Computable}\; (a \mapsto \mathrm{Option}.casesOn (o a) (f a) (g a))$$$
Lean4
theorem optionCasesOn_right {o : α → Option β} {f : α → σ} {g : α → β →. σ} (ho : Computable o) (hf : Computable f)
(hg : Partrec₂ g) : @Partrec _ σ _ _ fun a => Option.casesOn (o a) (Part.some (f a)) (g a) :=
have :
Partrec fun a : α => Nat.casesOn (encode (o a)) (Part.some (f a)) (fun n => Part.bind (decode (α := β) n) (g a)) :=
nat_casesOn_right (h := fun a n ↦ Part.bind (ofOption (decode n)) fun b ↦ g a b) (encode_iff.2 ho) hf.partrec <|
((@Computable.decode β _).comp snd).ofOption.bind (hg.comp (fst.comp fst) snd).to₂
this.of_eq fun a => by rcases o a with - | b <;> simp [encodek]
