proposition: Theorem HaltTM_to_MM_HALTING : HaltTM 1 ⪯ Halt_MM.
proof: Proof. eapply reduces_transitive. { exact HaltTM_1_to_SBTM_HALT.reduction. } eapply reduces_transitive. { exact SBTM_HALT_to_HaltBSM.reduction. } red. unfold reduction. setoid_rewrite <- BSM_sss.Halt_BSM_iff. exact BSM_MM_HALTING. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.MinskyMachines(MM MM_sss BSM_MM)