Library UnifConfl

Require Export ARS.

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

Uniform Confluence

  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 l1k2 l2 k1).

Uniform Diamond

  Definition uniform_diamond:= x y1 y2, x >> y1 x >> y2 y1 = y2 z, y1 >> z y2 >> z.

Proof of Equivalence

Characterization of Niehren

  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.

Uniform Confluence and Irreducible Terms

  Section UC.
  Variable UC:uniformly_confluent.

In the following, we assume thgat the Relation is uniform 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.