- ng_refiner:

[helm.git] / matita / matita / contribs / lambda / terms / parallel_reduction.ma

diff --git a/matita/matita/contribs/lambda/terms/parallel_reduction.ma b/matita/matita/contribs/lambda/terms/parallel_reduction.ma
index a9190151ba2a456f5854fbfedb0e5635e1feed1b..b54c4bc576bf22651af63b3b84073c4be9ae3e72 100644 (file)
--- a/matita/matita/contribs/lambda/terms/parallel_reduction.ma
+++ b/matita/matita/contribs/lambda/terms/parallel_reduction.ma
@@ -12,13 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "terms/length.ma".
-include "terms/labeled_sequential_reduction.ma".
+include "terms/size.ma".
+include "terms/sequential_reduction.ma".
 
 (* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
 
 (* Note: the application "(A B)" is represented by "@B.A"
-         as for labelled sequential reduction
+         as for sequential reduction
 *)
 inductive pred: relation term ≝
 | pred_vref: ∀i. pred (#i) (#i)
@@ -30,10 +30,6 @@ inductive pred: relation term ≝
 interpretation "parallel reduction"
     'ParRed M N = (pred M N).
 
-notation "hvbox( M ⤇ break term 46 N )"
-   non associative with precedence 45
-   for @{ 'ParRed $M $N }.
-
 lemma pred_refl: reflexive … pred.
 #M elim M -M // /2 width=1/
 qed.
@@ -115,8 +111,8 @@ qed-.
 
 lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … 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 *)
+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 *)
 elim (IH … HA1 … HA2) -A /3 width=3/
 qed-.
 
@@ -125,18 +121,18 @@ lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1.
                             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
-elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *)
+elim (pred_inv_abst … H1 …) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *)
 elim (IH B … HB1 … HB2) -HB1 -HB2 //
 elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
 qed-.
 
 theorem pred_conf: confluent … pred.
-#M @(f_ind … length … M) -M #n #IH * normalize
+#M @(f_ind … size … M) -M #n #IH * normalize
 [ /2 width=3 by pred_conf1_vref/
 | /3 width=4 by pred_conf1_abst/
 | #B #A #H #M1 #H1 #M2 #H2 destruct
-  elim (pred_inv_appl … H1 ???) -H1 [5: // |2,3: skip ] * (**) (* simplify line *)
-  elim (pred_inv_appl … H2 ???) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *) 
+  elim (pred_inv_appl … H1 …) -H1 [5: // |2,3: skip ] * (**) (* simplify line *)
+  elim (pred_inv_appl … H2 …) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *) 
   [ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct
     elim (IH A … HA1 … HA2) -HA1 -HA2 //
     elim (IH B … HB1 … HB2) // -A -B /3 width=5/
@@ -151,6 +147,6 @@ theorem pred_conf: confluent … pred.
 ]
 qed-.
 
-lemma lsred_pred: ∀p,M,N. M ↦[p] N → M ⤇ N.
-#p #M #N #H elim H -p -M -N /2 width=1/
+lemma sred_pred: ∀M,N. M ↦ N → M ⤇ N.
+#M #N #H elim H -M -N /2 width=1/
 qed.