proposition: Lemma decide_spec : decider decide MM_2_HALTING.
proof: Proof. rewrite /decider /reflects /decide => - [P v]. case: (decision P v). - tauto. - move=> H. split; [by move=> /H | done]. Qed.
imports: PeanoNat Lia List Undecidability.MinskyMachines(MM MM_sss) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions