proposition: Lemma uniform_decision_aux1 x : let n := l*(l+1) in (bounded (l*n*n+1) x) + { y | (exists k, k <= l*n*n /\ steps k x = Some y) /\ (n <= value1 y \/ n <= value2 y) }.
proof: Proof. move=> n. have [|/path_noloopI Hx] := In_dec option_mm2_state_eq_dec (steps (l*n*n) x) (path (l*n*n) x). { move=> /loop_bounded H. left. apply: (bounded_monotone _ H). lia. } case Hxy: (steps (l*n*n+1) x) => [y|]; first last. { left. by apply: mortal_bounded. } right. have [/pigeonhole|] := incl_dec option_mm2_state_eq_dec (path (l*n*n+1) x) (map Some (list_prod (seq 1 l) (list_prod (seq 0 n) (seq 0 n)))). { move=> H. exfalso. apply: (H _ Hx). rewrite path_length map_length ?prod_length ?seq_length. lia. } move=> /(not_inclE option_mm2_state_eq_dec) [[z|]]. - move=> H. exists z. move: H => [/in_map_iff] [k] [Hk] /in_seq ? H. split. { exists k. split; [lia|done]. } suff : not (value1 z < n /\ value2 z < n) by lia. move=> H'. apply: H. apply /in_map_iff. exists z. split; first done. have := steps_sub Hk Hxy ltac:(lia). have -> /=: l * n * n + 1 - k = S (Nat.pred (l * n * n + 1 - k)) by lia. case: (mm2_sig_step_dec M z) => [[?]|]; [|done]. move: z {Hk} H' => [? [? ?]] /= ? [?] /= [/mm2_instr_at_bounds ? _] _. apply /in_prod; [|apply /in_prod]; apply /in_seq; lia. - move=> [/in_map_iff] H. exfalso. move: H => [k] [+ /in_seq ?]. move=> /(steps_k_monotone (l*n*n+1)) /(_ ltac:(lia)). by rewrite Hxy. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun