X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fterms%2Fparallel_reduction.ma;h=17313b537ab2c9864f188f10b51a54b2c32179c2;hb=613d8642b1154dde0c026cbdcd96568910198251;hp=b54c4bc576bf22651af63b3b84073c4be9ae3e72;hpb=aa9654656f7d0aeb9345e0b86a9e35f861687580;p=helm.git

diff --git a/matita/matita/lib/lambda/terms/parallel_reduction.ma b/matita/matita/lib/lambda/terms/parallel_reduction.ma
index b54c4bc57..17313b537 100644
--- a/matita/matita/lib/lambda/terms/parallel_reduction.ma
+++ b/matita/matita/lib/lambda/terms/parallel_reduction.ma
@@ -12,8 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "terms/size.ma".
-include "terms/sequential_reduction.ma".
+include "lambda/terms/size.ma".
+include "lambda/terms/sequential_reduction.ma".
+
+include "lambda/notation/relations/parred_2.ma".
+
+include "lambda/xoa/ex_4_3.ma".
 
 (* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
 
@@ -102,14 +106,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 +121,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