proposition: Lemma MMA2_HALTS_ON_ZERO_undec : undecidable MMA2_HALTS_ON_ZERO.
proof: Proof. apply (undecidability_from_reducibility FRACTRAN_REG_undec). apply FRACTRAN_REG_MMA2_HALTS_ON_ZERO. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.FRACTRAN(FRACTRAN FRACTRAN_undec) Undecidability.MinskyMachines(MMA FRACTRAN_to_MMA2)