proposition: Lemma mm2_steps_terminates_r {P x y} : P // x ↠ y -> P // x ↓ -> P // y ↓.
proof: Proof. move=> Hxy [z] [Hxz Hz]. have [z' [Hyz' Hzz']] := mm2_steps_confluent Hxy Hxz. apply: (mm2_steps_terminates_l Hyz'). move: Hzz' (Hz) => /mm2_steps_stop_refl /[apply] ->. by apply: mm2_stop_terminates. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun