proposition: Lemma SBTM_HALT_enumeration : { e : nat -> option { M : SBTM & config M } | enumerator e SBTM_HALT }.
proof: Proof. exact (semi_decider_enumerator (proj2_sig SBTM_HALT_INSTANCE_enumeration) (proj2_sig SBTM_HALT_semi_decision)). Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts) Undecidability.TM.SBTM