X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flcosx_cpx.ma;h=eaa8649d4c70232410a3ca724bb07bcfb8ea3db0;hb=4b8544042a6f3c5f5d303d4120c69abbc34ce15b;hp=8583b9dea5ff7b541644eb0162680bf1503bbce3;hpb=52e675f555f559c047d5449db7fc89a51b977d35;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma
index 8583b9dea..eaa8649d4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpx.ma
@@ -23,42 +23,43 @@ include "basic_2/computation/lcosx.ma".
 (* Properties on extended context-sensitive parallel reduction for term *****)
 
 lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
-                           ∀d. G ⊢ ~⬊*[h, g, d] L →
-                           G ⊢ ⬊*[h, g, T1, d] L → G ⊢ ⬊*[h, g, T2, d] L.
+                           ∀l. G ⊢ ~⬊*[h, g, l] L →
+                           G ⊢ ⬊*[h, g, T1, l] L → G ⊢ ⬊*[h, g, T2, l] L.
 #h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
-[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #HL #H
-  elim (ylt_split i d) #Hdi [ -H | -HL ]
-  [ <(ymax_pre_sn d (⫯i)) /2 width=1 by ylt_fwd_le_succ/
-    elim (lcosx_drop_trans_lt … HL … HLK) // -HL -Hdi
+[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #l #HL #H
+  elim (ylt_split i l) #Hli [ -H | -HL ]
+  [ <(ymax_pre_sn l (⫯i)) /2 width=1 by ylt_fwd_le_succ1/
+    elim (lcosx_drop_trans_lt … HL … HLK) // -HL -Hli
     lapply (drop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
-  | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hdi
+  | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hli
     lapply (drop_fwd_drop2 … HLK) -HLK
     /4 width=10 by lsx_ge, lsx_lift_le/
   ]
-| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H
+| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
   elim (lsx_inv_bind … H) -H #HV1 #HT1
   @lsx_bind /2 width=2 by/ (**) (* explicit constructor *)
-  @(lsx_leq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, leq_succ/
-| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H
+  @(lsx_lreq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, lreq_succ/
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
   elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/
-| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #d #HL #H
-  elim (lsx_inv_bind … H) -H
-  /4 width=9 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
-| #G #L #V #T1 #T2 #_ #IHT12 #d #HL #H
+| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #l #HL #H
+  elim (lsx_inv_bind … H) -H #HV #HU1
+  <(ypred_succ l) <yminus_SO2
+  /4 width=7 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
+| #G #L #V #T1 #T2 #_ #IHT12 #l #HL #H
   elim (lsx_inv_flat … H) -H /2 width=1 by/
-| #G #L #V1 #V2 #T #_ #IHV12 #d #HL #H
+| #G #L #V1 #V2 #T #_ #IHV12 #l #HL #H
   elim (lsx_inv_flat … H) -H /2 width=1 by/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #l #HL #H
   elim (lsx_inv_flat … H) -H #HV1 #H
   elim (lsx_inv_bind … H) -H #HW1 #HT1
   @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *)
-  @(lsx_leq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, leq_succ/
-| #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H
+  @(lsx_lreq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, lreq_succ/
+| #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #l #HL #H
   elim (lsx_inv_flat … H) -H #HV1 #H
   elim (lsx_inv_bind … H) -H #HW1 #HT1
   @lsx_bind /2 width=1 by/ (**) (* explicit constructor *)
-  @lsx_flat [ /3 width=7 by lsx_lift_ge, drop_drop/ ]
-  @(lsx_leq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, leq_succ/
+  @lsx_flat [ <yplus_SO2 /3 width=7 by lsx_lift_ge, drop_drop/ ]
+  @(lsx_lreq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, lreq_succ/
 ]
 qed-.