proposition: Lemma decide_spec : decider decide MM2_UMORTAL.
proof: Proof. rewrite /decider /reflects /decide => M. case: (decision M); intuition done. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties ConstructiveEpsilon Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Deciders.MM2_UBOUNDED_dec Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions