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