proposition: Lemma bound_on_uniform_bound : mm2_uniformly_bounded M -> forall x, bounded ((l+1)*(l+1)*(l+1)*(l+1)*(l+1)) x.
proof: Proof. move=> HM x. set K := ((l+1)*(l+1)*(l+1)*(l+1)*(l+1)). have [|[y [[k1 [Hk1 Hxy]] ?]]] := uniform_decision_aux1 x. { apply: bounded_monotone. lia. } have -> : K = k1 + (K - k1) by lia. apply: (reaches_bounded Hxy). have : {l * (l + 1) <= value1 y} + {l * (l + 1) <= value2 y}. { case H: (l * (l + 1) - value1 y) => [|?]; [left|right]; lia. } move=> /uniform_decision_aux2 [[|]|[z]]. - apply: bounded_monotone. lia. - by move=> /(_ HM). - move=> [[k2 [? Hyz]]] [/uniform_decision_aux3 H /H{H}]. move=> [/bounded_monotone Hz|]. + have -> : K - k1 = k2 + (K - k1 - k2) by lia. apply: (reaches_bounded Hyz). apply: Hz. lia. + by move=> /(_ HM). Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun