Notation "p '<=1' q" := (∀ x, p x → q x) (at level 70).
Notation "p '=1' q" := (p <=1 q ∧ q <=1 p) (at level 70).
Notation "R '<=2' S" := (∀ x y, R x y → S x y) (at level 70).
Notation "R '=2' S" := (R <=2 S ∧ S <=2 R) (at level 70).

Definition rcomp X Y Z (R : X → Y → Prop) (S : Y → Z → Prop)
: X → Z → Prop :=
  fun x z ⇒ ∃ y, R x y ∧ S y z.

Definition pow X R n : X → X → Prop := it (rcomp R) n eq.

Section FixX.
  Variable X : Type.
  Implicit Types R S : X → X → Prop.
  Implicit Types x y z : X.

  Definition reflexive R := ∀ x, R x x.
  Definition symmetric R := ∀ x y, R x y → R y x.
  Definition transitive R := ∀ x y z, R x y → R y z → R x z.
  Definition functional R := ∀ x y z, R x y → R x z → y = z.

  Inductive star R : X → X → Prop :=
  | starR x : star R x x
  | starC x y z : R x y → star R y z → star R x z.


  Lemma star_simpl_ind R (p : X → Prop) y :
    p y →
    (∀ x x', R x x' → star R x' y → p x' → p x) →
    ∀ x, star R x y → p x.

  Lemma star_trans R:
    transitive (star R).

  Lemma star_pow R x y :
    star R x y ↔ ∃ n, pow R n x y.

  Inductive ecl R : X → X → Prop :=
  | eclR x : ecl R x x
  | eclC x y z : R x y → ecl R y z → ecl R x z
  | eclS x y z : R y x → ecl R y z → ecl R x z.

  Lemma ecl_trans R :
    transitive (ecl R).

  Lemma ecl_sym R :
    symmetric (ecl R).

  Lemma star_ecl R :
    star R <=2 ecl R.

  Definition joinable R x y :=
    ∃ z, R x z ∧ R y z.

  Definition diamond R :=
    ∀ x y z, R x y → R x z → joinable R y z.

  Definition confluent R := diamond (star R).

  Definition semi_confluent R :=
    ∀ x y z, R x y → star R x z → joinable (star R) y z.

  Definition church_rosser R :=
    ecl R <=2 joinable (star R).

  Goal ∀ R, diamond R → semi_confluent R.

  Lemma diamond_to_semi_confluent R :
    diamond R → semi_confluent R.

  Lemma semi_confluent_confluent R :
    semi_confluent R ↔ confluent R.

  Lemma diamond_to_confluent R :
    diamond R → confluent R.

  Lemma confluent_CR R :
    church_rosser R ↔ confluent R.

  Definition uniform_confluent (R : X → X → Prop ) := ∀ s t1 t2, R s t1 → R s t2 → t1 = t2 ∨ ∃ u, R t1 u ∧ R t2 u.

  Lemma pow_add R n m (s t : X) : pow R (n + m) s t ↔ rcomp (pow R n) (pow R m) s t.

  Lemma rcomp_eq (R S R' S' : X → X → Prop) (s t : X) : (R =2 R') → (S =2 S') → (rcomp R S s t ↔ rcomp R' S' s t).

  Lemma eq_ref : ∀ (R : X → X → Prop), R =2 R.

  Lemma rcomp_1 (R : X → X → Prop): R =2 pow R 1.

  Lemma parametrized_semi_confluence (R : X → X → Prop) (m : nat) (s t1 t2 : X) :
    uniform_confluent R →
    pow R m s t1 →
    R s t2 →
    ∃ k l u,
      k ≤ 1 ∧ l ≤ m ∧ pow R k t1 u ∧ pow R l t2 u ∧ m + k = S l.

  Lemma rcomp_comm R m (s t : X) : rcomp R (it (rcomp R) m eq) s t ↔ rcomp (it (rcomp R) m eq) R s t.

  Lemma parametrized_confluence (R : X → X → Prop) (m n : nat) (s t1 t2 : X) :
    uniform_confluent R →
    pow R m s t1 →
    pow R n s t2 →
    ∃ k l u,
      k ≤ n ∧ l ≤ m ∧ pow R k t1 u ∧ pow R l t2 u ∧ m + k = n + l.

End FixX.