proposition: Lemma init_M : Nat.iter (a0 + b0 + b0) (CM1.step M) {| CM1.state := 0; CM1.value := 1 |} = {| CM1.state := a0 + b0 + b0; CM1.value := κ a0 b0 0 |}.
proof: Proof. rewrite /Nat.iter Nat.add_comm nat_rect_plus -!/(Nat.iter _ _ _) init_M_a0. { done. } rewrite init_M_b0. { done. } rewrite (Nat.add_comm b0). 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