AFTD Auto-Formalizing Theoretical Domains

re_complete_of_le

theoremverified

If p is RE-complete, q is recursively enumerable, and p many-one reduces to q, then q is RE-complete.

Statement

universe u in
theorem re_complete_of_le {α β : Type*} [Primcodable α] [Primcodable β]
    {p : α → Prop} {q : β → Prop} (hp : REComplete.{_, u} p) (hq : REPred q) (h : p ≤₀ q) :
    REComplete.{_, u} q
Verified
06 Sep 2026
Axioms
Classical.choiceQuot.soundpropext
Built on 1
  • RECompleteA predicate `p` is RE-complete if it is recursively enumerable and every recursively enumerable predicate many-one reduces to `p`.

Lean source view module on GitHub

universe u in
/-- If p is RE-complete, q is RE, and p ≤₀ q, then q is RE-complete (for predicates in the same universe). -/
theorem re_complete_of_le {α β : Type*} [Primcodable α] [Primcodable β]
    {p : α → Prop} {q : β → Prop} (hp : REComplete.{_, u} p) (hq : REPred q) (h : p ≤₀ q) :
    REComplete.{_, u} q := ⟨hq, fun _ hr => (hp.2 _ hr).trans h⟩
Discuss this resultChallenge it