English
A general version of merge' for functions of higher type, detailing how to build a witness function that preserves domains and membership relations.
Русский
Обобщённая версия merge' для функций высшего типа, описывающая как построить свидетеля, сохраняющего домены и отношение принадлежности.
LaTeX
$$/* generalized merge' statement for higher-types */$$
Lean4
nonrec theorem sumCasesOn {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ →. σ} (hf : Computable f) (hg : Partrec₂ g)
(hh : Partrec₂ h) : @Partrec _ σ _ _ fun a => Sum.casesOn (f a) (g a) (h a) :=
option_some_iff.1 <|
(cond (sumCasesOn hf (const true).to₂ (const false).to₂)
(sumCasesOn_left hf (option_some_iff.2 hg).to₂ (const Option.none).to₂)
(sumCasesOn_right hf (const Option.none).to₂ (option_some_iff.2 hh).to₂)).of_eq
fun a => by cases f a <;> simp only [Bool.cond_true, Bool.cond_false]
