X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Frelations.ma;h=3d67a576c412dc8c8ab59abd5e7535e9082922ec;hp=98e14be386c44279c3472fac7114cb8460c2aa52;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hpb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground/lib/relations.ma
index 98e14be38..3d67a576c 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/relations.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/relations.ma
@@ -72,6 +72,9 @@ definition transitive2 (A) (R1,R2:relation A): Prop ≝
            ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
            ∃∃a. R2 a1 a & R1 a a2.
 
+definition confluent1 (A) (B): relation2 (relation2 A B) (relation A) ≝
+           λR1,R2. ∀a1,b. R1 a1 b → ∀a2. R2 a1 a2 → R1 a2 b.
+
 definition bi_confluent (A) (B) (R: bi_relation A B): Prop ≝
            ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 →
            ∃∃a,b. R a1 b1 a b & R a2 b2 a b.