proposition: Theorem decision : (mm2_uniformly_bounded M) + (not (mm2_uniformly_bounded M)).
proof: Proof. wlog ? : /(l > 0). { move: (M) => [|? ?] /=. - move=> _. left. by apply: uniformly_bounded_empty. - apply. lia. } pose K := (l+1)*(l+1)*(l+1)*(l+1)*(l+1). have [?|HK] := fixed_decision K. { left. by exists K. } right. move=> /bound_on_uniform_bound => HM. apply: HK => x. by apply: HM. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun