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