- cprs and cnx on the way

[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 bf7f3b11f4d13410e142e063b4e5f2c99a740756..26832eb42c295a5110c36a34794b42979612126d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
@@ -17,6 +17,12 @@ include "ground_2/xoa/xoa_props.ma".
 
 (* PROPERTIES OF RELATIONS **************************************************)
 
+definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
+≝ λA,B,C,D,E.A→B→C→D→E→Prop.
+
+definition relation6 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
+≝ λA,B,C,D,E,F.A→B→C→D→E→F→Prop.
+
 definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥).
 
 definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R.
@@ -28,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 →
@@ -126,14 +135,14 @@ lemma TC_transitive2: ∀A,R1,R2.
 qed.
 
 definition NF: ∀A. relation A → relation A → predicate A ≝
-   λA,R,S,a1. ∀a2. R a1 a2 → S a2 a1.
+   λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
 
 definition NF_dec: ∀A. relation A → relation A → Prop ≝
                    λA,R,S. ∀a1. NF A R S a1 ∨
-                   ∃∃a2. R … a1 a2 & (S a2 a1 → ⊥).
+                   ∃∃a2. R … a1 a2 & (S a1 a2 → ⊥).
 
 inductive SN (A) (R,S:relation A): predicate A ≝
-| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a2 a1 → ⊥) → SN A R S a2) → SN A R S a1
+| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → ⊥) → SN A R S a2) → SN A R S a1
 .
 
 lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
@@ -151,10 +160,10 @@ lemma SN_to_NF: ∀A,R,S. NF_dec A R S →
 qed-.
 
 definition NF_sn: ∀A. relation A → relation A → predicate A ≝
-   λA,R,S,a2. ∀a1. R a1 a2 → S a2 a1.
+   λA,R,S,a2. ∀a1. R a1 a2 → S a1 a2.
 
 inductive SN_sn (A) (R,S:relation A): predicate A ≝
-| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a2 a1 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2
+| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a1 a2 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2
 .
 
 lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.