proposition: Lemma not_uniformly_boundedI k p a1 b1 a2 b2 : (k <= a1 \/ a1 = a2) -> (k <= b1 \/ b1 = b2) -> (a1 <> a2 \/ b1 <> b2) -> steps k (p, (a1, b1)) = Some (p, (a2, b2)) -> not (mm2_uniformly_bounded M).
proof: Proof. move=> /k_step_iter H /H {}H Hab /H /= + [K]. move=> /(_ _ K 0 0) /=. move Ha: (a1 + _ * _) => a. move Hb: (b1 + _ * _) => b. move=> {}H /(_ (p, (a, b))) [L [? HL]]. have : incl (map (fun i => steps (i * k) (p, (a, b))) (seq 0 (K+1))) (map Some L). { move=> z /in_map_iff [i] [<- /in_seq ?]. rewrite H; first by lia. apply: in_map. apply: HL. apply: (steps_reaches (k := (i*k))). rewrite H; [lia|done]. } move=> /pigeonhole. apply. { rewrite ?map_length seq_length. lia. } under map_ext_in. { move=> i /in_seq ?. rewrite H; first by lia. over. } apply: NoDup_map_ext; last by apply: seq_NoDup. move=> i1 /in_seq ? i2 /in_seq ? []. move: (Nat.eq_dec a1 a2) (Nat.eq_dec b1 b2) => [?|?] [?|?] /=; nia. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun