proposition: Lemma init_M_a0 (n: nat) : n <= a0+b0 -> Nat.iter n (CM1.step M) {| CM1.state := 0; CM1.value := 1 |} = {| CM1.state := n; CM1.value := κ n 0 0 |}.
proof: Proof. elim: n. { done. } move=> n /= + ? => ->. { lia. } rewrite /M /= κ_pos. rewrite nth_error_app1. { by rewrite map_length seq_length. } rewrite nth_error_map nth_error_seq /=. { done. } by rewrite κ_norm. 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