proposition: Lemma uniform_decision_aux3 x : l <= value1 x -> l <= value2 x -> (bounded (l+1) x) + (not (mm2_uniformly_bounded M)).
proof: Proof. move=> ??. have [|/path_noloopI Hx] := In_dec option_mm2_state_eq_dec (steps (l) x) (path (l) x). { move=> /loop_bounded H. left. apply: (bounded_monotone _ H). lia. } case Hxy: (steps (l+1) x) => [y|]; first last. { left. by apply: mortal_bounded. } right. have /pigeonhole : incl (map (fun oz => if oz is Some (p, (a, b)) then p else 0) (path (l + 1) x)) (seq 1 l). { move=> p /in_map_iff [[[p' [a' b']]|]]; first last. { move=> [_ /In_pathE]. move=> [?] [?] /(steps_k_monotone (l + 1)) /(_ ltac:(lia)). by rewrite Hxy. } move=> [->] H. apply /in_seq. move: H => /in_map_iff [k'] [Hk' /in_seq ?]. have := steps_sub Hk' Hxy ltac:(lia). have -> /=: l + 1 - k' = S (l + 1 - k' - 1) by lia. case: (mm2_sig_step_dec M (p, (a', b'))) => [[?]|]; [|done]. move=> [?] [/mm2_instr_at_bounds] /=. lia. } apply: unnest. { rewrite map_length ?seq_length path_length. lia. } rewrite /path map_map. move=> /(dup_seq Nat.eq_dec) [[i j]]. move=> [+ ?]. case Hi: (steps i x) => [[p [a1 b1]]|]; first last. { move: Hi => /(steps_k_monotone (l+1)) /(_ ltac:(lia)). by rewrite Hxy. } case Hj: (steps j x) => [[p' [a2 b2]]|]; first last. { move: Hj => /(steps_k_monotone (l+1)) /(_ ltac:(lia)). by rewrite Hxy. } move=> ?. subst p'. have ? : a1 <> a2 \/ b1 <> b2. { suff : not (a1 = a2 /\ b1 = b2) by lia. move=> [??]. subst a2 b2. move: Hx. rewrite /path. have -> : l+1 = i + (S (j-i-1)) + (S (l -j)) by lia. rewrite seq_app seq_app /= ?map_app /= (NoDup_count_occ option_mm2_state_eq_dec). move=> /(_ (Some (p, (a1, b1)))). have ->: i + S (j - i - 1) = j by lia. rewrite Hi Hj ?count_occ_app /=. case: (option_mm2_state_eq_dec _ _); [lia|done]. } have ?: j - i <= a1 /\ j - i <= b1. { move: Hi => /steps_values_bound /=. lia. } have := steps_sub Hi Hj ltac:(lia). move=> /not_uniformly_boundedI. apply; lia. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun