X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Frelations.ma;h=84dd7c362bf7a86e590fc474130372bbc5e703f7;hb=07f64a04ac6061c853d2e60237a7173968c6d759;hp=f469ddca29f72fe1eeaeea9d50752fefed34aad2;hpb=a04bfe6d381b281db15e8b432f6f221576aad439;p=helm.git diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index f469ddca2..84dd7c362 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -48,6 +48,24 @@ definition tight_apart: ∀A.∀eq,ap:relation A.Prop definition antisymmetric: ∀A.∀R:relation A.Prop ≝ λA.λR.∀x,y:A. R x y → ¬(R y x). +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 ≝ + λA,R,x,y. R … x y ∨ x = y. + +lemma RC_reflexive: ∀A,R. reflexive A (RC … R). +/2 width=1/ qed. + (********** operations **********) definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2. ∃am.R1 a1 am ∧ R2 am a2.