proposition: Lemma dec_b_0 x n : reaches' (1, (1, 1)) x -> step x (1, (1 + n, 0)) -> forall a b, reaches (1, (a, b)) (1, (b * n + a, 0)).
proof: Proof. move=> H1x H2x a b. elim: b a. - move=> a. by apply: rt_refl. - move=> b IH a. move: H1x => /reaches'E [n'] [m'] /= [Hax] [Hbx]. move=> /(_ (a) (S b) ltac:(lia) ltac:(lia)). move=> /reaches'_incl /rt_trans. apply. have ->: n + b * n + a = b * n + (n + a) by lia. apply: (rt_trans _ (IH (n + a))). apply: rt_step. move Ey: (1, (1 + n, 0)) H2x => y Hxy. move: Hxy Ey => [i] [+ Hxy] => /[dup] /mm2_instr_at_pos. case: Hxy Hax Hbx => /=. 1,2,3,5,6: by congruence. move=> i' j' a' b' -> [->] -> Hi [] *. subst j' n' m'. eexists. split; [eassumption|]. have [-> ->]: b + 0 = b /\ a + n = n + a by lia. by constructor. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun