proposition: Lemma MM2_ZERO_HALTING_undec : undecidable MM2_ZERO_HALTING.
proof: Proof. apply (undecidability_from_reducibility MM2_HALTING_undec). exact MM2_HALTING_to_MM2_ZERO_HALTING.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.MinskyMachines(MMA MM2 MMA2_undec MMA2_to_MM2)