proposition: Lemma cm1_steps n x : clos_refl_trans _ cm1_step x (Nat.iter n (CM1.step M) x).
proof: Proof. elim: n. { apply: rt_refl. } move=> n IH /=. have [<-|?] := Config_eq_dec (Nat.iter n (CM1.step M) x) (CM1.step M (Nat.iter n (CM1.step M) x)). { done. } apply: rt_trans. - by apply: IH. - by apply: rt_step. 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