X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_csx_vector.ma;h=30f35f70fef5a1de10d690f9e4fbaf2d6b9cc9dd;hb=5c92c318030a05c766b3f6070dbd23589cbdee04;hp=fa81a32d258d33a03deccad8b99f39dc4629f6b1;hpb=43998467c5ec5f1c8e1e988fc00e3255d2723ba4;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
index fa81a32d2..30f35f70f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
@@ -15,10 +15,10 @@
 include "basic_2/rt_computation/cpxs_theq_vector.ma".
 include "basic_2/rt_computation/csx_simple_theq.ma".
 include "basic_2/rt_computation/csx_lsubr.ma".
-include "basic_2/rt_computation/csx_lfpx.ma".
+include "basic_2/rt_computation/csx_lpx.ma".
 include "basic_2/rt_computation/csx_vector.ma".
 
-(* STRONGLY NORMALIZING TERM VECTORS FOR UNCOUNTED PARALLEL RT-TRANSITION ***)
+(* STRONGLY NORMALIZING TERM VECTORS FOR UNBOUND PARALLEL RT-TRANSITION *****)
 
 (* Advanced properties ************************************* ****************)
 
@@ -37,11 +37,11 @@ elim (cpxs_fwd_beta_vector … o … H) -H #H
 ]
 qed.
 
-lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 →
-                       ∀V2. ⬆*[⫯i] V1 ≡ V2 →
+lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
+                       ∀V2. ⬆*[↑i] V1 ≘ V2 →
                        ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.V2⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.#i⦄.
 #h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
-[ /4 width=11 by csx_inv_lifts, csx_lref_drops, drops_isuni_fwd_drop2/
+[ /4 width=11 by csx_inv_lifts, csx_lref_pair, drops_isuni_fwd_drop2/
 | #V #Vs #IHV #H1T
   lapply (csx_fwd_pair_sn … H1T) #HV
   lapply (csx_fwd_flat_dx … H1T) #H2T
@@ -55,7 +55,7 @@ lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇*[i] L ≡ K.ⓑ{I}V1 →
 qed.
 
 (* Basic_1: was just: sn3_appls_abbr *)
-lemma csx_applv_theta: ∀h,o,p,G,L,V1b,V2b. ⬆*[1] V1b ≡ V2b →
+lemma csx_applv_theta: ∀h,o,p,G,L,V1b,V2b. ⬆*[1] V1b ≘ V2b →
                        ∀V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.ⒶV2b.T⦄ →
                        ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶV1b.ⓓ{p}V.T⦄.
 #h #o #p #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/
@@ -67,7 +67,7 @@ lapply (csx_appl_theta … H … HW12) -H -HW12 #H
 lapply (csx_fwd_pair_sn … H) #HW1
 lapply (csx_fwd_flat_dx … H) #H1
 @csx_appl_simple_theq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2
-elim (cpxs_fwd_theta_vector … o … (V2@V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
+elim (cpxs_fwd_theta_vector … o … (V2⨮V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
 [ -H #H elim H2 -H2 //
 | -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
 ]