Require Export ARS.

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

  Definition uniformly_confluent :=
    ∀ x y1 y2 k1 k2,
      x >^k1 y1 → x >^k2 y2 →
      ∃ z l1 l2 , y1 >^l1 z ∧ y2 >^l2 z ∧ (k1 + l1 = k2 + l2 ∧ l1≤k2 ∧ l2 ≤ k1).

  Definition uniform_diamond:= ∀ x y1 y2, x >> y1 → x >> y2 → y1 = y2 ∨ ∃ z, y1 >> z ∧ y2 >> z.

  Lemma uniformly_semi_confluent x y1 y2 k:
    uniform_diamond →
    x >> y1 →
    x >^ k y2 →
    ∃ z l1 l2, y1 >^l1 z ∧ y2 >^ l2 z ∧ (l2 ≤ 1 ∧ l1 ≤ k ∧ 1+l1=k+l2).

  Lemma UD_UC : uniform_diamond → uniformly_confluent.

  Lemma UC_DC : uniformly_confluent → uniform_diamond.

  Lemma UC_confluent: uniformly_confluent → confluent R.

  Definition UC_niehren :=
    ∀ x y1 y2 k1 k2 , x>^k1 y1 → x>^k2 y2 →
                           ∃ z m, m ≤ min k1 k2 ∧ y1 >^(k2-m) z ∧ y2 >^(k1-m) z.

  Lemma UC_niehren_iff:
    UC_niehren ↔ uniformly_confluent.

  Definition irred x := ∀ y, ¬ x >> y.

  Lemma irred_pow x y k : irred x → x >^k y → k=0.

  Section UC.
  Variable UC:uniformly_confluent.

  Lemma unif_pow_normal_part x y z k1 k2:
    irred y → x >^k1 y → x >^k2 z → k2 ≤ k1 ∧ z >^(k1-k2) y.

  Lemma unif_pow_normal x y k1 k2: irred y → x >^k1 y → x >^k2 y → k1=k2.

  Lemma unif_unique x y1 y2 k1 k2: irred y1 → irred y2 → x >^k1 y1 → x >^k2 y2 → k1=k2 ∧ y1 = y2.
  End UC.
End FixX.