proposition: Theorem decision (M: list mm2_instr) : (mm2_uniformly_mortal M) + (not (mm2_uniformly_mortal M)).
proof: Proof. case: (MM2_UBOUNDED_dec.decision M). - move=> /constructive_indefinite_ground_description. move=> /(_ id id (fun=> erefl) (MM2_UBOUNDED_dec.fixed_decision M)). by move=> [K /uniform_decision]. - move=> H. right. move=> [k Hk]. apply: H. exists (S k) => x. apply: mortal_bounded. by apply /mortal_steps_iff. 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