proposition: Lemma dec_a_0 x m : reaches' (1, (1, 1)) x -> step x (1, (0, 1 + m)) -> forall a b, reaches (1, (a, b)) (1, (0, a * m + b)).
proof: Proof. move=> H1x H2x. elim. - move=> b. by apply: rt_refl. - move=> a IH b. move: H1x => /reaches'E [n'] [m'] /= [Hax] [Hbx]. move=> /(_ (S a) b ltac:(lia) ltac:(lia)). move=> /reaches'_incl /rt_trans. apply. have ->: m + a * m + b = a * m + (m + b) by lia. apply: (rt_trans _ (IH (m + b))). apply: rt_step. move Ey: (1, (0, 1 + m)) H2x => y Hxy. move: Hxy Ey => [i] [+ Hxy] => /[dup] /mm2_instr_at_pos. case: Hxy Hax Hbx => /=. 1,2,4,5,6: by congruence. move=> i' j' a' b' [->] -> -> Hi [] *. subst j' n' m'. eexists. split; [eassumption|]. have [-> ->]: a + 0 = a /\ b + m = m + b 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