# 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.

# 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.

# Irreducibility

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.