X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fterms%2Fparallel_reduction.ma;h=b2d2c2ff9ec8cecbe1aff9e1cd7af37b269b9ea3;hp=111d794b013ec92cb59b02d74c95668ce58ac01d;hb=3a4509b8e569181979f5b15808361c83eb1ae49a;hpb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a

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