proposition: Theorem FRACTRAN_REG_undec : undecidable FRACTRAN_REG_HALTING.
proof: Proof. apply (undecidability_from_reducibility MM_HALTING_undec). apply MM_FRACTRAN_REG_HALTING. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.MinskyMachines(MM MM_undec) Undecidability.FRACTRAN(FRACTRAN Reductions.MM_FRACTRAN FRACTRAN_sss)