re_pred_or
theoremverified
If p and q are recursively enumerable predicates, then their disjunction fun a => p a ∨ q a is recursively enumerable.
Statement
theorem re_pred_or {α : Type*} [Primcodable α] {p q : α → Prop} (hp : REPred p) (hq : REPred q) : REPred (fun a => p a ∨ q a)
- Verified
- 06 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext
Lean source view module on GitHub
/-- The disjunction of two recursively enumerable predicates is recursively enumerable. -/ theorem re_pred_or {α : Type*} [Primcodable α] {p q : α → Prop} (hp : REPred p) (hq : REPred q) : REPred (fun a => p a ∨ q a) := by obtain ⟨k, hk, hdom⟩ := Partrec.merge' hp hq have h_re : REPred (fun a => (k a).Dom) := hk.dom_re refine h_re.of_eq fun a => ?_ rw [(hdom a).2] simp [Part.assert]