proposition: Theorem Newman : forall (U:Type) (R:Relation U), Noetherian U R -> Locally_confluent U R -> Confluent U R.
proof: Proof. intros U R H' H'0; red; intro x. elim (H' x); unfold confluent. intros x0 H'1 H'2 y z H'3 H'4. generalize (Rstar_cases U R x0 y); intro h; lapply h; [ intro h0; elim h0; [ clear h h0; intro h1 | intro h1; elim h1; intros u h2; elim h2; intros H'5 H'6; clear h h0 h1 h2 ] | clear h ]; auto with sets. - elim h1; auto with sets. - generalize (Rstar_cases U R x0 z); intro h; lapply h; [ intro h0; elim h0; [ clear h h0; intro h1 | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8; clear h h0 h1 h2 ] | clear h ]; auto with sets. + elim h1; generalize coherent_symmetric; intro t; red in t; auto with sets. + unfold Locally_confluent, locally_confluent, coherent in H'0. generalize (H'0 x0 u v); intro h; lapply h; [ intro H'9; lapply H'9; [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11; clear h H'9 h0 h1 | clear h ] | clear h ]; auto with sets. clear H'0. unfold coherent at 1 in H'2. generalize (H'2 u); intro h; lapply h; [ intro H'0; generalize (H'0 y t); intro h0; lapply h0; [ intro H'9; lapply H'9; [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13; clear h h0 H'9 h1 h2 | clear h h0 ] | clear h h0 ] | clear h ]; auto with sets. generalize Rstar_transitive; intro T; red in T. generalize (H'2 v); intro h; lapply h; [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0; [ intro H'14; lapply H'14; [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16; clear h h0 H'14 h1 h2 | clear h h0 ] | clear h h0 ] | clear h ]; auto with sets. * red; (exists z1; split); auto with sets. apply T with y1; auto with sets. * apply T with t; auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2 Relations_2_facts Relations_3