Require Import PCF2.external.Synthetic.Undecidability.
From PCF2.external.Synthetic Require Import DecidabilityFacts EnumerabilityFacts.
Require Import PCF2.external.TM.SBTM.
Require PCF2.external.TM.SBTM_HALT_enum.


Lemma complement_SBTM_HALT_undec :
  undecidable (complement SBTM_HALT).
Proof.
  intros H.
  eapply (dec_count_enum H), enumerator_enumerable.
  apply enumerator__T_sigT.
  - now apply (proj2_sig SBTM_HALT_enum.SBTM_enumeration).
  - intros M. now apply (proj2_sig (SBTM_HALT_enum.config_enumeration M)).
Qed.


Lemma SBTM_HALT_undec :
  undecidable SBTM_HALT.
Proof.
  intros H. now apply complement_SBTM_HALT_undec, dec_compl.
Qed.