English
Let f: α → β ⊕ γ, g: α → β → σ, h: α → γ → σ. If f, g, h are primitive recursive (with the given arities), then the function a ↦ Sum.casesOn (f a) (g a) (h a) is primitive recursive.
Русский
Пусть f: α → β ⊕ γ, g: α → β → σ, h: α → γ → σ. Если эти отображения примитивно вычислимы, то функция a ↦ Sum.casesOn (f a) (g a) (h a) является примитивно вычислимой.
LaTeX
$$$\\mathrm{Primrec}\\left( a \\mapsto \\mathrm{Sum.casesOn}\\left( f(a) \\right) \\left( g(a) \\right) \\left( h(a) \\right) \\right)$$$
Lean4
theorem sumCasesOn {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ} (hf : Primrec f) (hg : Primrec₂ g)
(hh : Primrec₂ h) : @Primrec _ σ _ _ fun a => Sum.casesOn (f a) (g a) (h a) :=
option_some_iff.1 <|
(cond (nat_bodd.comp <| encode_iff.2 hf) (option_map (Primrec.decode.comp <| nat_div2.comp <| encode_iff.2 hf) hh)
(option_map (Primrec.decode.comp <| nat_div2.comp <| encode_iff.2 hf) hg)).of_eq
fun a => by rcases f a with b | c <;> simp [Nat.div2_val, encodek]
