proposition: Lemma MM_HALTS_ON_ZERO_undec : undecidable MM_HALTS_ON_ZERO.
proof: Proof. apply (undecidability_from_reducibility BSM_undec). apply BSM_MM_HALTS_ON_ZERO. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.StackMachines(BSM BSM_undec) Undecidability.MinskyMachines(MM MM_sss Reductions.BSM_MM)