proposition: Lemma init_a0 n : n <= a0 -> mm2'_reaches (1, (0, 0)) (1+n, (n, 0)).
proof: Proof. elim: n. { move=> _. by apply: rt_refl. } move=> n IH ?. apply: rt_trans; [|apply: rt_step]. - apply: IH. lia. - exists mm2_inc_a. split; [|constructor]. rewrite /M'. apply /nth_error_Some_mm2_instr_at_iff. rewrite nth_error_app1. { by rewrite repeat_length. } by apply: nth_error_repeat. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun