proposition: Lemma HaltMTM_undec : undecidable HaltMTM.
proof: Proof. apply (undecidability_from_reducibility SBTM_HALT_undec). apply (reduces_transitive SBTM_HALT_to_HaltTM_1.reduction). apply nTM_to_MTM. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.TM.Reductions.mTM_to_TM Undecidability.TM.Reductions.SBTM_HALT_to_HaltTM_1 Undecidability.TM.SBTM_undec