Variable A : Set.
Variable a : A.
Variable R : A -> A -> Prop.

Inductive RR : A -> A -> Prop :=
| RR_refl : (x,z:A) x=z -> (RR x z)
| RR_trans : (x,y,z:A) (R x y) -> (RR y z) -> (RR x z).

Inductive Rstar : A->A->Prop :=
|Rstar_cont_eq : (x,y:A)x=y->(Rstar x y)
|Rstar_cont_R : (x,y:A)(R x y)->(Rstar x y)
|Rstar_trans : (x,y,z:A)(Rstar x y)->(Rstar y z)->(Rstar x z).

Lemma equiv: (x,y:A)(RR x y)<->(Rstar x y).
Intros x y.
Split.
Intro.
Print RR_ind.
Elim H.
Intros.
Apply (Rstar_cont_eq x0 z).
Auto.
Intros.
Apply (Rstar_trans x0 y0 z).
Apply (Rstar_cont_R x0 y0).
Auto.
Auto.
Intro.
Print Rstar_ind.
Elim H.
Induction 1 ; Apply RR_refl.
Trivial.
Intros c b rab ; Apply RR_trans with b.
Exact rab.
Apply RR_refl.
Trivial.
Intros x0 y0 z H1 H2.
Elim H2.
Induction 1 ; Trivial.
Intros.
Apply RR_trans with y1.
Auto.
Auto.
Qed.

Definition lconfl_pred :=
[x:A](y,z:A) ((R x y) /\ (R x z)) -> (EX u:A | ((RR y u) /\ (RR z u))).

Definition lCONFL := (x:A)(lconfl_pred x).

Definition confl_pred :=
 [x:A](y,z:A) ((RR x y) /\ (RR x z))
   -> (EX u:A | ((RR y u) /\ (RR z u))).
 
Definition CONFL := (x:A)(confl_pred x).

Inductive Acc : A -> Prop :=
 acc : (x:A)((y:A)(R x y)->(Acc y))->(Acc x). 

Definition SN := (x:A)(Acc x). 

Lemma CasesRR: (x,z:A) (RR x z) -> (x=z \/ (EX y:A | (R x y) /\ (RR y z))).
Proof.
Intros x z H.
Elim H. Clear H x z. 
Intros x z H. Left. Assumption.
Intros.
Right.
Exists y. Split; Assumption.
Qed.

Lemma TransRR: (x,y,z:A) (RR x y)->(RR y z)->(RR x z).
Intros x y z H.
Elim H.
Induction 1.
Auto.
Intros.
Apply (RR_trans x0 y0 z).
Auto.
Apply H2.
Auto.
Qed.

Lemma Newman: SN -> lCONFL -> CONFL.
Unfold SN.
Intro sn.
Unfold lCONFL.
Intro lconfl.
Unfold CONFL.
Intro z.
Check Acc_ind.
Apply Acc_ind.
2:Apply sn.
Intro x.
Intro U.
Intro IH.
Unfold confl_pred.
Intro x1.
Intro x2.
Intro Div_x1x2.
Unfold lconfl_pred in lconfl.
Elim Div_x1x2.
Intro X1.
Intro X2.
Cut (x=x1 \/ x=x2 \/
((EX y1:A | (R x y1) /\ (RR y1 x1)) /\ (EX y2:A | (R x y2) /\ (RR y2 x2)))). 
Intro Disj1. 
Elim Disj1. Intro E1. Exists x2. Split. Elim E1. Assumption.
Apply RR_refl. Trivial.
Intro Disj2. 
Elim Disj2. Intro E2. Exists x1. Split. Apply RR_refl. Trivial.
Elim E2. Assumption.
Intro Conj. Elim Conj. Intros P1 P2.
Elim P1. Elim P2.
Intros y2 Conj2 y1 Conj1.
Elim Conj1. Intros Rxy1 RRy1x1.
Elim Conj2. Intros Rxy2 RRy2x2.
Cut (EX u:A | (RR y1 u)/\(RR y2 u)). Intro Lconfl. Elim Lconfl.
Intros y Conj3. Elim Conj3. Intros RRy1y RRy2y.
Cut (EX y3:A | (RR x1 y3) /\ (RR y2 y3)). Intro IHy2.
Elim IHy2. Intros y3 Conj4. Elim Conj4. Intros RRx1y3 RRy2y3.
Cut (EX y4:A | (RR y3 y4) /\ (RR x2 y4)). Intro Joiny3x2.
Elim Joiny3x2. Intros y4 Conj5. Elim Conj5. Intros RRy3y4 RRx2y4.
Exists y4. Split. Exact (TransRR x1 y3 y4 RRx1y3 RRy3y4). Assumption.
Unfold confl_pred in IH.
Apply (IH y2 Rxy2 y3 x2). Split ; Assumption.
Cut (EX y3:A | (RR x1 y3) /\ (RR y y3)). Intro Joinx1y.
Elim Joinx1y. Intros y3 Conj6. Elim Conj6. Intros RRx1y3 RRyy3.
Exists y3. Split. Assumption. Exact (TransRR y2 y y3 RRy2y RRyy3). 
Apply (IH y1 Rxy1 x1 y). Split; Assumption.
Apply (lconfl x y1 y2). Split; Assumption.
Elim (CasesRR x x1 X1). Intro. Left. Assumption. Intro Path1.
Elim (CasesRR x x2 X2). Intro. Right. Left. Assumption. Intro Path2.
Right. Right. Split; Assumption.
Qed.