proposition: Theorem Strong_confluence_direct : forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R.
proof: Proof. intros U R H'; red. intro x; red; intros a b H'0. unfold coherent at 1. generalize b; clear b. elim H'0; clear H'0. - intros x0 b H'1; exists b; auto with sets. - intros x0 y z H'1 H'2 H'3 b H'4. cut (ex (fun t:U => Rstar U R y t /\ R b t)). + intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0. generalize (H'3 t); intro h; lapply h; [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1 | clear h ]; auto with sets. exists z0; split; [ assumption | idtac ]. apply Rstar_n with t; auto with sets. + generalize H'1; generalize y; clear H'1. elim H'4. * intros x1 y0 H'0; exists y0; auto with sets. * intros x1 y0 z0 H'0 H'1 H'5 y1 H'6. red in H'. generalize (H' x1 y0 y1); intro h; lapply h; [ intro H'7; lapply H'7; [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h H'7 h0 h1 | clear h ] | clear h ]; auto with sets. generalize (H'5 z1); intro h; lapply h; [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1 | clear h ]; auto with sets. exists t; split; auto with sets. apply Rstar_n with z1; auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2 Relations_2_facts Relations_3