X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Frelations.ma;h=84dd7c362bf7a86e590fc474130372bbc5e703f7;hb=3a9c3c16e7c7e3a35640a0afa53f044a4f87ed65;hp=8b746ef6896d4f58bb4efa17728a27b7f8bba0e7;hpb=5e24c923ea53c31c3e167c4ff7851877ded646c1;p=helm.git

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 8b746ef68..84dd7c362 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -51,6 +51,13 @@ definition antisymmetric: ∀A.∀R:relation A.Prop
 definition singlevalued: ∀A,B. predicate (relation2 A B) ≝ λA,B,R.
                          ∀a,b1. R a b1 → ∀b2. R a b2 → b1 = b2.
 
+definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
+                       ∀a1. R a0 a1 → ∀a2. R a0 a2 →
+                       ∃∃a. R a1 a & R a2 a. 
+
+definition confluent: ∀A. predicate (relation A) ≝ λA,R.
+                      ∀a0. confluent1 … R a0.
+
 (* Reflexive closure ************)
 
 definition RC: ∀A:Type[0]. relation A → relation A ≝