Require Import Undecidability.Synthetic.Undecidability.
From Undecidability.MinskyMachines
Require Import MM2 MM2_undec ndMM2 MM2_to_ndMM2_ACCEPT.
Theorem ndMM2_undec : undecidable (@ndMM2_ACCEPT nat).
Proof.
apply (undecidability_from_reducibility MM2_HALTS_ON_ZERO_undec).
apply MM2_to_ndMM2_ACCEPT.reduction.
Qed.