proposition: Lemma reflection : MM2_ZERO_HALTING M' -> MM2_HALTING (M, a0, b0).
proof: Proof. move=> [y'] [Hxy' Hy']. have Hinit := init_a0b0. have Hx'y' : mm2'_reaches (shift_state (1, (a0, b0))) y'. { have [z [/mm2_steps_stop_refl Hyz Hinitz]] := mm2_steps_confluent Hxy' Hinit. by rewrite -(Hyz Hy'). } have Hsim := sim.terminates_reflection (@mm2_step_det M') mm2_step_sim' (mm2_exists_step_dec M). apply: (Hsim _ _ erefl). by exists y'. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun