proposition: Lemma init_M_b0 (n: nat) : n <= b0 -> Nat.iter n (CM1.step M) {| CM1.state := a0 + b0; CM1.value := κ (a0+b0) 0 0 |} = {| CM1.state := a0 + b0 + n; CM1.value := κ (a0 + b0 - n) n 0 |}.
proof: Proof. elim: n. { by rewrite Nat.sub_0_r Nat.add_0_r. } move=> n /= + ? => ->. { lia. } rewrite /M /= κ_pos. rewrite nth_error_app2 map_length seq_length. { lia. } rewrite nth_error_app1. { rewrite map_length seq_length. lia. } rewrite nth_error_map nth_error_seq /=. { lia. } rewrite κ_norm. have ->: a0 + b0 - n = S (a0 + b0 - n - 1) by lia. rewrite κ_norm. congr CM1.mkConfig; [|congr κ]; lia. Qed.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun