proposition: Fact diamond_semi_confluent R : diamond R -> semi_confluent R.
proof: Proof. intros H x y1 y2 H1 H2. revert y1 H1. induction H2 as [x|x x' y2 H2 _ IH]; intros y1 H1. - exists y1; eauto. - assert (joinable R y1 x') as [z H3 H4]. { eapply H; eauto. } assert (joinable (star R) z y2) as [u H5 H6]. { apply IH; auto. } exists u; eauto. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics std.misc std.ars.basic)