Proof of `RE is not closed under complement` (1st statement)
groundedproofs/Lax624099Proofs/Bridge.lean · lax-624099
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Were the complement of code halting recursively enumerable, code halting would be decidable by Post's theorem, against the library's undecidability of code halting; recursive enumerability on concrete instances is this submission's statement.