proposition: Lemma fixed_decision K : {forall x : mm2_state, bounded K x} + {~ (forall x : mm2_state, bounded K x)}.
proof: Proof. have := Forall_dec (fun 'x => bounded K x) (pointwise_decision K) (list_prod (seq 1 l) (list_prod (seq 0 (K+1)) (seq 0 (K+1)))). case; first last. { move=> H. right => HK. apply /H /Forall_forall. move=> ??. by apply: HK. } wlog: K /(0 < K). { move: K => [|K] H HK. - right. move=> /(_ (0, (0, 0))) [[|? L] [/= ? /(_ (0, (0, 0))) HL]]. + apply: HL. by apply: rt_refl. + lia. - apply: H; [lia|done]. } move=> ? HK. left => x. have [|/path_noloopI] := In_dec option_mm2_state_eq_dec (steps K x) (path K x). { by apply: loop_bounded. } case Hz: (steps K x) => [z|]; first last. { move=> _. by apply: mortal_bounded. } move=> Hx. exfalso. move: x Hx Hz => [p [a b]] Hx Hz. have Hp : 0 < p <= l. { move: Hz. have -> : K = 1 + (K - 1) by lia. rewrite steps_plus' /=. case: (mm2_sig_step_dec M (p, (a, b))) => [[?]|]; last done. by move=> [?] [/mm2_instr_at_bounds] /=. } move: Hx Hz. wlog: a b z /(a <= K /\ b <= K); first last. { move=> ? Hx Hz. suff: bounded K (p, (a, b)). { by apply: (NoDup_not_bounded Hz). } move: HK => /Forall_forall. apply. apply: in_prod; [|apply: in_prod]; apply /in_seq; lia. } move=> H'K. wlog: a b z /(a <= K). { move=> H. have [/H|->] : a <= K \/ a = K + (a - K) by lia. { by apply. } move=> /path_NoDup_a_bound => /(_ ltac:(lia)) /H {H}. rewrite shift_steps_a; first done. case: (steps K (p, (K, b))) => [y|]; last done. move=> H _. by apply: (H y). } move=> ?. have [?|->] : b <= K \/ b = K + (b - K) by lia. { move=> /H'K H /H. by apply. } move=> /path_NoDup_b_bound => /(_ ltac:(lia)) /H'K. rewrite shift_steps_b; first done. case: (steps K (p, (a, K))) => [y|]; last done. move=> H _. by apply: (H y). Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun