proposition: Lemma mm2_steps_confluent {P x y1 y2} : P // x ↠ y1 -> P // x ↠ y2 -> exists z, P // y1 ↠ z /\ P // y2 ↠ z.
proof: Proof. move=> /clos_rt_rt1n_iff H. elim: H y2. - move=> *. eexists. by split; [|apply rt_refl]. - move=> ? {}y1 z1 Hx /clos_rt_rt1n_iff Hyz IH ? /clos_rt_rt1n_iff Hxy2. case: Hxy2 Hx IH. + move=> ? _. eexists. split; [apply: rt_refl|]. apply: rt_trans; [apply: rt_step|]; by eassumption. + move=> y2 z2 /mm2_step_det Hx /clos_rt_rt1n_iff Hy2z2 /Hx {Hx} ? IH. subst y2. move: Hy2z2 => /IH [z [??]]. by exists z. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun