proposition: Lemma uniform_decision : (mm2_uniformly_mortal M) + (not (mm2_uniformly_mortal M)).
proof: Proof. Proof using HK. have := Forall_dec (fun 'x => mortal K x) _ (list_prod (seq 1 (length M)) (list_prod (seq 0 (K+2)) (seq 0 (K+2)))). case. { move=> x. by apply: pointwise_decision. } - move=> H'M. left. exists K => - [p [a b]]. have [?|?] : (p = 0 \/ length M < p) \/ 0 < p <= length M by lia. { move=> [|??] /=; first by lia. move=> [[?]] [/mm2_instr_at_bounds] /=. lia. } apply /mortal_K_bound. move: H'M => /Forall_forall. apply. apply /in_prod. { apply /in_seq. lia. } apply /in_prod; apply /in_seq; lia. - move=> H. right => - [K' H'M]. apply: H. apply /Forall_forall. move=> [p [a b]] /in_prod_iff [/in_seq ?] /in_prod_iff [/in_seq ?] /in_seq ?. apply: (bounded_mortal_bound _ (H'M _)). apply: (bounded_monotone _ _ (HK _)). lia. 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