improved lexs_conf, now holds under weaker hypotheses ...

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / lib / star.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
index 8849d759beeaf774379ecc33015d548353b6e913..b0e3e6be601368d027e964864d73c371eb1bb8d3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
@@ -34,9 +34,12 @@ definition left_cancellable: ∀A. ∀R: relation A. Prop ≝ λA,R.
 definition right_cancellable: ∀A. ∀R: relation A. Prop ≝ λA,R.
                               ∀a1,a0. R a1 a0 → ∀a2. R a2 a0 → R a1 a2.
 
-definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
-                       ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
-                       ∃∃a. R2 a1 a & R1 a2 a.
+definition pw_confluent2: ∀A. relation A → relation A → predicate A ≝ λA,R1,R2,a0.
+                          ∀a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
+                          ∃∃a. R2 a1 a & R1 a2 a.
+
+definition confluent2: ∀A. relation (relation A) ≝ λA,R1,R2.
+                       ∀a0. pw_confluent2 A R1 R2 a0.
 
 definition transitive2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
                         ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →