X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpxs_drops.ma;h=c42f94f83b665ee43394297b61cda43a7aa5fd6a;hp=0fd54e95ac94f0c5ab05ba76c7f6b96bd971fb46;hb=ff612dc35167ec0c145864c9aa8ae5e1ebe20a48;hpb=75f395f0febd02de8e0f881d918a8812b1425c8d

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
index 0fd54e95a..c42f94f83 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/drops_lstar.ma".
+include "static_2/relocation/drops_ctc.ma".
 include "basic_2/rt_transition/cpx_drops.ma".
 include "basic_2/rt_computation/cpxs.ma".
 
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
 
 (* Advanced properties ******************************************************)
 
@@ -31,7 +31,7 @@ lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
 qed.
 
 lemma cpxs_lref: ∀h,I,G,K,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T →
-                 ∀U. ⬆*[1] T ≘ U → ⦃G, K.ⓘ{I}⦄ ⊢ #⫯i ⬈*[h] U.
+                 ∀U. ⬆*[1] T ≘ U → ⦃G, K.ⓘ{I}⦄ ⊢ #↑i ⬈*[h] U.
 #h #I #G #K #T #i #H @(cpxs_ind … H) -T
 [ /3 width=3 by cpx_cpxs, cpx_lref/
 | #T0 #T #_ #HT2 #IH #U #HTU
@@ -43,11 +43,11 @@ qed.
 (* Basic_2A1: was: cpxs_delta *)
 lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.
                         ⬇*[i] L ≘ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
-                        ∀W2. ⬆*[⫯i] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h] W2.
+                        ∀W2. ⬆*[↑i] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h] W2.
 #h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
 [ /3 width=7 by cpx_cpxs, cpx_delta_drops/
 | #V #V2 #_ #HV2 #IH #W2 #HVW2
-  elim (lifts_total V (𝐔❴⫯i❵))
+  elim (lifts_total V (𝐔❴↑i❵))
   /4 width=11 by cpxs_strap1, cpx_lifts_bi, drops_isuni_fwd_drop2/
 ]
 qed.
@@ -69,8 +69,8 @@ lemma cpxs_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈*[h] T2 →
 ]
 qed-.
 
-lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈*[h] T2 →
-                      T2 = #(⫯i) ∨
+lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #↑i ⬈*[h] T2 →
+                      T2 = #(↑i) ∨
                       ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ⬈*[h] T & ⬆*[1] T ≘ T2 & L = K.ⓘ{I}.
 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
 #T #T2 #_ #HT2 *
@@ -87,7 +87,7 @@ qed-.
 lemma cpxs_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h] T2 →
                             T2 = #i ∨
                             ∃∃I,K,V1,T1. ⬇*[i] L ≘ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h] T1 &
-                                         ⬆*[⫯i] T1 ≘ T2.
+                                         ⬆*[↑i] T1 ≘ T2.
 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
 #T #T2 #_ #HT2 *
 [ #H destruct