Require Import Relations.
Require Import Confluence.
Require Import Coherence.
Require Import Noetherian.

Set Implicit Arguments.
Unset Strict Implicit.

Theorem Newman :
 ∀ (U : Type) (R : Relation U),
 Noetherian R → Locally_confluent R → Confluent R.
Proof.
intros U R H' H'0; red in |- *; intro x; red in |- ×.
red in H'; generalize (H' x); intro H'1; elim H'1.
intros x0 H'2 H'3 y z H'4 H'5; clear H' H'1.
generalize (Rstar_cases (U:=U) (R:=R) (x:=x0) (y:=y)); intro h; lapply h;
 [ intro H'6; clear h | clear h; assumption ].
generalize (Rstar_cases (U:=U) (R:=R) (x:=x0) (y:=z)); intro h; lapply h;
 [ intro H'7; clear h | clear h; assumption ].
elim H'6;
 [ clear H'6; intro h
 | intro h; elim h; intros u h0; elim h0; intros H' H'1; clear H'6 h h0 ].
rewrite <- h; auto.
elim H'7;
 [ clear H'7; intro h
 | intro h; elim h; intros v h0; elim h0; intros H'6 H'8; clear H'7 h h0 ].
rewrite <- h; generalize coherent_symmetric; intro H_cs; red in H_cs; auto.
unfold Locally_confluent, locally_confluent, coherent in H'0.
generalize (H'0 x0 u v); intro h; lapply h;
 [ intro H'7; lapply H'7;
    [ intro h0; elim h0; intros t h1; elim h1; intros H'9 H'10;
       clear h H'7 h0 h1
    | clear h ]
 | clear h ]; auto.
clear H'0.
unfold coherent at 1 in H'3.
generalize (H'3 u); intro h; lapply h;
 [ intro H'0; generalize (H'0 y t); intro h0; lapply h0;
    [ intro H'7; lapply H'7;
       [ intro h1; elim h1; intros y1 h2; elim h2; intros H'11 H'12;
          clear h h0 H'7 h1 h2
       | clear h h0 ]
    | clear h h0 ]
 | clear h ]; auto.
generalize Rstar_transitive; intro H_Rst; red in H_Rst.
generalize (H'3 v); intro h; lapply h;
 [ intro H'7; generalize (H'7 y1 z); intro h0; lapply h0;
    [ intro H'13; lapply H'13;
       [ intro h1; elim h1; intros z1 h2; elim h2; intros H'14 H'15;
          clear h h0 H'13 h1 h2
       | clear h h0 ]
    | clear h h0 ]
 | clear h ]; auto.
red in |- *; (∃ z1; split); auto.
apply H_Rst with y1; auto.
apply H_Rst with t; auto.
Qed.