proposition: Lemma cm1_halting_stuck x : CM1.halting M x -> deterministic_simulation.stuck cm1_step x.
proof: Proof. rewrite /CM1.halting. move=> Hx y [Hxy H'xy]. congruence. 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