proposition: Lemma dec_loop x n m : reaches' (1, (1, 1)) x -> step x (1, (1 + n, 1 + m)) -> forall a b, non_terminating (1, (a, b)).
proof: Proof. move=> H0x Hx0. suff: forall a b, exists a' b', reaches_plus (1, (a, b)) (1, (a', b')). { move=> H a b. pose P := fun (x : mm2_state) => index x = 1. apply: (mm2_clos_trans_not_terminates P _ (1, (a, b)) erefl). move=> [p' [a' b']]. rewrite /P /= => ?. have [a'' [b'' H'']] := H a' b'. subst p'. eexists. by split; [eassumption|]. } move=> a b. move: (H0x) => /reaches'E [n'] [m'] /= [Hax] [Hbx]. move=> /(_ a b ltac:(lia) ltac:(lia)). move=> /reaches'_incl /clos_rt_t H'. move: Hx0 => [i] [/[dup] Hi /mm2_instr_at_pos H''x]. move Ey: (1, (1 + n, 1 + m)) => y Hxy. case: Hxy H''x Ey Hi H' Hax Hbx => > /=. 1,2,5,6: by congruence. - move=> -> [<- <- <-] Hi H' [?] [?]. subst n' m'. exists (a + n), (b + m). apply: H'. apply: t_step. have -> : a + S n = S (a + n) by lia. by apply: (mm2_step_intro Hi (S (a + n)) (b + m)). - move=> -> [<- <- <-] Hi H' [?] [?]. subst n' m'. exists (a + n), (b + m). apply: H'. apply: t_step. have -> : b + S m = S (b + m) by lia. by apply: (mm2_step_intro Hi (a + n) (S (b + m))). Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun