proposition: Lemma transport : MM2_HALTING (M, a0, b0) -> MM2_ZERO_HALTING M'.
proof: Proof. have Hsim := sim.terminates_transport mm2_step_sim' mm2_stuck_sim'. move=> /Hsim => /(_ _ erefl) [y [Hxy Hy]]. exists y. split; [|done]. by apply: rt_trans; [apply: init_a0b0|apply: Hxy]. Qed.
imports: List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun