proposition: Corollary MM_FRACTRAN_HALTING : Halt_MM ⪯ Halt_FRACTRAN.
proof: Proof. eapply reduces_transitive. apply MM_FRACTRAN_ALT_HALTING. exact FRACTRAN_ALT_HALTING_HALTING. Qed.
imports: Undecidability.Shared.Libs.DLW(pos vec sss) Undecidability.MinskyMachines(mm_defs) Undecidability.FRACTRAN(FRACTRAN fractran_utils mm_fractran prime_seq FRACTRAN_sss) Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts