proposition: Lemma mm2_stuck_sim' x x' : sim.stuck (mm2_step M) x -> sync x x' -> sim.terminates (mm2_step M') x'.
proof: Proof. rewrite /sync => /mm2_stop_index_iff Hx <-. exists (shift_state x). split; [apply: rt_refl|]. apply /mm2_stop_index_iff. rewrite length_M'. move: x Hx => [[|p] [a b]] /=; lia. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun