proposition: Lemma HaltTM_to_FRACTRAN_REG_HALTING : HaltTM 1 ⪯ FRACTRAN_REG_HALTING.
proof: Proof. apply (reduces_transitive HaltTM_to_MM_HALTING). exact MM_FRACTRAN_REG_HALTING. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.MinskyMachines(MM HaltTM_1_to_MM) Undecidability.FRACTRAN(FRACTRAN Reductions.MM_FRACTRAN FRACTRAN_sss)