proposition: Lemma decide_spec : decider decide MM2_REV_HALT.
proof: Proof. rewrite /decider /reflects /decide => - [[M HM] c]. case: (decision M HM c). - tauto. - move=> H. split; [by move=> /H | done]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions