proposition: Theorem MM_2_HALTING_dec : decidable MM_2_HALTING.
proof: Proof. exists MM_2_HALTING_dec.decide. exact MM_2_HALTING_dec.decide_spec. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.MinskyMachines(MM MM_sss)