From 3a4509b8e569181979f5b15808361c83eb1ae49a Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 9 Apr 2020 15:52:50 +0200
Subject: [PATCH] renaming in basics/relations
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

+ we rename adefinition that was clashing with λδ
---
 matita/matita/lib/basics/relations.ma                | 8 ++++----
 matita/matita/lib/lambda/terms/parallel_reduction.ma | 6 +++---
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 3133682db..9da779ee4 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -56,12 +56,12 @@ 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 pw_confluent: ∀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.
+                      ∀a0. pw_confluent … R a0.
 
 (* triangular confluence of two relations *)
 definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.
diff --git a/matita/matita/lib/lambda/terms/parallel_reduction.ma b/matita/matita/lib/lambda/terms/parallel_reduction.ma
index 111d794b0..b2d2c2ff9 100644
--- a/matita/matita/lib/lambda/terms/parallel_reduction.ma
+++ b/matita/matita/lib/lambda/terms/parallel_reduction.ma
@@ -102,14 +102,14 @@ lemma pred_dsubst: dsubstable pred.
 ]
 qed.
 
-lemma pred_conf1_vref: ∀i. confluent1 … pred (#i).
+lemma pred_conf1_vref: ∀i. pw_confluent … pred (#i).
 #i #M1 #H1 #M2 #H2
 <(pred_inv_vref … H1) -H1 [3: // |2: skip ] (**) (* simplify line *)
 <(pred_inv_vref … H2) -H2 [3: // |2: skip ] (**) (* simplify line *)
 /2 width=3/
 qed-.
 
-lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A).
+lemma pred_conf1_abst: ∀A. pw_confluent … pred A → pw_confluent … pred (𝛌.A).
 #A #IH #M1 #H1 #M2 #H2
 elim (pred_inv_abst … H1 …) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *)
 elim (pred_inv_abst … H2 …) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *)
@@ -117,7 +117,7 @@ elim (IH … HA1 … HA2) -A /3 width=3/
 qed-.
 
 lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1.
-                            (∀M0. |M0| < |B|+|𝛌.C|+1 → confluent1 ? pred M0) → (**) (* ? needed in place of … *)
+                            (∀M0. |M0| < |B|+|𝛌.C|+1 →  pw_confluent ? pred M0) → (**) (* ? needed in place of … *)
                             B ⤇ B1 → B ⤇ B2 → 𝛌.C ⤇ M1 → C ⤇ C2 →
                             ∃∃M. @B1.M1 ⤇ M & [↙B2]C2 ⤇ M.
 #B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2
-- 
2.39.2