proposition: Lemma uniform_decision_aux2 x : ({l*(l+1) <= value1 x} + {l*(l+1) <= value2 x}) -> (bounded (l*l+1) x) + (not (mm2_uniformly_bounded M)) + { y | (exists k, k <= l*l /\ steps k x = Some y) /\ (l <= value1 y /\ l <= value2 y) }.
proof: Proof. move=> Hlx. have [|/path_noloopI Hx] := In_dec option_mm2_state_eq_dec (steps (l*l) x) (path (l*l) x). { move=> /loop_bounded H. left. left. apply: (bounded_monotone _ H). lia. } case Hxy: (steps (l*l+1) x) => [y|]; first last. { left. left. by apply: mortal_bounded. } pose P := fun oz : option mm2_state => if oz is Some z then (if Hlx then l <= value2 z else l <= value1 z) else True. have HP : forall x, {P x} + {not (P x)}. { move=> [? /= |]; last by left. clear P. case: Hlx => ?; by apply: Compare_dec.le_dec. } have [|H'x] := Exists_dec P (path (l * l + 1) x) HP. { move=> /(Exists_sig P HP) [[z|]] [Hz /= H'z]. - right. exists z. move: Hz => /In_pathE [k [? Hk]]. split. + exists k. split; [lia|done]. + move: Hk => /steps_values_bound. clear P HP. case: Hlx H'z => /=; lia. - exfalso. by move: Hz Hxy => /In_None_pathE ->. } left. right. subst P. have /pigeonhole : incl (map (fun oz => if oz is Some (p, (a, b)) then (if Hlx then (p, b) else (p, a)) else (0, 0)) (path (l * l + 1) x)) (list_prod (seq 1 l) (seq 0 l)). { move=> [p c] /in_map_iff [[[p' [a' b']]|]]; first last. { move=> [_ /In_pathE]. move=> [?] [?] /(steps_k_monotone (l * l + 1)) /(_ ltac:(lia)). by rewrite Hxy. } move=> [+ H]. have ? : 0 < p' <= l. { move: H => /in_map_iff [k'] [Hk' /in_seq ?]. have := steps_sub Hk' Hxy ltac:(lia). have -> /=: l * l + 1 - k' = S (l * l + 1 - k' - 1) by lia. case: (mm2_sig_step_dec M (p', (a', b'))) => [[?]|]; [|done]. by move=> [?] [/mm2_instr_at_bounds]. } case: Hlx H'x HP => /= ? H'x HP. - move=> [? ?]. subst p c. move: H'x H => /Forall_Exists_neg /Forall_forall H /H{H} /= ?. apply /in_prod; apply /in_seq; lia. - move=> [? ?]. subst p c. move: H'x H => /Forall_Exists_neg /Forall_forall H /H{H} /= ?. apply /in_prod; apply /in_seq; lia. } apply: unnest. { rewrite map_length ?prod_length ?seq_length path_length. lia. } rewrite /path map_map. move=> /(dup_seq prod_nat_nat_eq_dec) [[i j]]. move=> [+ ?]. case Hi: (steps i x) => [[p [a1 b1]]|]; first last. { move: Hi => /(steps_k_monotone (l*l+1)) /(_ ltac:(lia)). by rewrite Hxy. } case Hj: (steps j x) => [[p' [a2 b2]]|]; first last. { move: Hj => /(steps_k_monotone (l*l+1)) /(_ ltac:(lia)). by rewrite Hxy. } clear H'x. have ? : not (p = p' /\ a1 = a2 /\ b1 = b2). { move=> [? [? ?]]. subst p' a2 b2. move: Hx. rewrite /path. have -> : l*l+1 = i + (S (j-i-1)) + (S (l*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]. } case: Hlx HP => /= ? HP. - move=> [? ?]. subst p' b2. have ? : a1 <> a2 by lia. have ? : j-i <= a1. { move: Hi => /steps_values_bound /=. lia. } move: Hi Hj => /steps_sub H /H{H} /(_ ltac:(lia)). move /not_uniformly_boundedI. apply; lia. - move=> [? ?]. subst p' a2. have ? : b1 <> b2 by lia. have ? : j-i <= b1. { move: Hi => /steps_values_bound /=. lia. } move: Hi Hj => /steps_sub H /H{H} /(_ 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