English
If α and β are primitive codable, then α ⊕ β is primitive codable.
Русский
Если α и β примитивно кодируемы, то α ⊕ β примитивно кодируемо.
LaTeX
$$$\\text{Primcodable}(\\alpha\\oplus\\beta)$ given $\\text{Primcodable}(\\alpha)$ and $\\text{Primcodable}(\\beta)$.$$
Lean4
instance sum : Primcodable (α ⊕ β) :=
⟨Primrec.nat_iff.1 <|
(encode_iff.2
(cond nat_bodd
(((@Primrec.decode β _).comp nat_div2).option_map <|
to₂ <| nat_double_succ.comp (Primrec.encode.comp snd))
(((@Primrec.decode α _).comp nat_div2).option_map <|
to₂ <| nat_double.comp (Primrec.encode.comp snd)))).of_eq
fun n =>
show _ = encode (decodeSum n) by
simp only [decodeSum, Nat.boddDiv2_eq]
cases Nat.bodd n <;> simp
· cases @decode α _ n.div2 <;> rfl
· cases @decode β _ n.div2 <;> rfl⟩
