Require Import Undecidability.Synthetic.Undecidability.
Require Import Undecidability.TM.TM.

Require Import Undecidability.TM.Reductions.mTM_to_TM.

HaltMTM and HaltTM 1 are undecidable

Lemma HaltTM_1_undec :
  undecidable (HaltTM 1).
Proof.
  intros d. exact d.
Qed.

Lemma HaltTM_1_compl_undec :
  mundecidable (complement (HaltTM 1)).
Proof.
  apply mundecidability_HaltTM_compl.
Qed.

Lemma HaltMTM_undec :
  undecidable HaltMTM.
Proof.
  apply (undecidability_from_reducibility HaltTM_1_undec).
  eapply nTM_to_MTM.
Qed.