proposition: Theorem ndMM2_undec : undecidable (@ndMM2_ACCEPT nat).
proof: Proof. apply (undecidability_from_reducibility MMA2_HALTS_ON_ZERO_undec). apply MMA2_to_ndMM2_ACCEPT.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.MinskyMachines(MMA MMA2_undec ndMM2 MMA2_to_ndMM2_ACCEPT)