proposition: Theorem FRACTRAN_undec : undecidable Halt_FRACTRAN.
proof: Proof. apply (undecidability_from_reducibility FRACTRAN_REG_undec). apply FRACTRAN_REG_FRACTRAN_HALTING. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.MinskyMachines(MM MM_undec) Undecidability.FRACTRAN(FRACTRAN Reductions.MM_FRACTRAN FRACTRAN_sss)