REComplete
def
A predicate `p` is RE-complete if it is recursively enumerable and every recursively enumerable predicate many-one reduces to `p`.
Statement
def REComplete {α : Type*} [Primcodable α] (p : α → Prop) : Prop
- Verified
- 06 Sep 2026
- Axioms
- none listed
- Used by 1
- re_complete_of_leIf p is RE-complete, q is recursively enumerable, and p many-one reduces to q, then q is RE-complete.
Lean source view module on GitHub
/-- A predicate on a primcodable type is RE-complete if it is RE and every RE predicate is many-one reducible to it. -/ def REComplete {α : Type*} [Primcodable α] (p : α → Prop) : Prop := REPred p ∧ ∀ {β : Type*} [Primcodable β] (q : β → Prop), REPred q → q ≤₀ p