syntactic components detached from basic_2 become static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpxs_drops.ma

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 99a6e3670fa6a35bc25c4aa0cae731d4e4805d76..c42f94f83b665ee43394297b61cda43a7aa5fd6a 100644 (file)
--- 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,16 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-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 ******************************************************)
 
 lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
-                  â\88\80W2. â¬\86*[1] V2 â\89¡ W2 → ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈*[h] W2.
+                  â\88\80W2. â¬\86*[1] V2 â\89\98 W2 → ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈*[h] W2.
 #h #I #G #K #V1 #V2 #H @(cpxs_ind … H) -V2
 [ /3 width=3 by cpx_cpxs, cpx_delta/
 | #V #V2 #_ #HV2 #IH #W2 #HVW2
@@ -30,9 +30,9 @@ lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
 ]
 qed.
 
-lemma cpxs_lref: ∀h,I,G,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T →
-                 â\88\80U. â¬\86*[1] T â\89¡ U â\86\92 â¦\83G, K.â\93\91{I}Vâ¦\84 â\8a¢ #⫯i ⬈*[h] U.
-#h #I #G #K #V #T #i #H @(cpxs_ind … H) -T
+lemma cpxs_lref: ∀h,I,G,K,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T →
+                 â\88\80U. â¬\86*[1] T â\89\98 U â\86\92 â¦\83G, K.â\93\98{I}â¦\84 â\8a¢ #â\86\91i ⬈*[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
   elim (lifts_total T0 (𝐔❴1❵))
@@ -42,12 +42,12 @@ qed.
 
 (* Basic_2A1: was: cpxs_delta *)
 lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.
-                        â¬\87*[i] L â\89¡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
-                        â\88\80W2. â¬\86*[⫯i] V2 â\89¡ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h] W2.
+                        â¬\87*[i] L â\89\98 K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 →
+                        â\88\80W2. â¬\86*[â\86\91i] V2 â\89\98 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 (ð\9d\90\94â\9d´â«¯i❵))
+  elim (lifts_total V (ð\9d\90\94â\9d´â\86\91i❵))
   /4 width=11 by cpxs_strap1, cpx_lifts_bi, drops_isuni_fwd_drop2/
 ]
 qed.
@@ -56,7 +56,7 @@ qed.
 
 lemma cpxs_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈*[h] T2 →
                       T2 = #0 ∨
-                      â\88\83â\88\83I,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88*[h] V2 & â¬\86*[1] V2 â\89¡ T2 &
+                      â\88\83â\88\83I,K,V1,V2. â¦\83G, Kâ¦\84 â\8a¢ V1 â¬\88*[h] V2 & â¬\86*[1] V2 â\89\98 T2 &
                                    L = K.ⓑ{I}V1.
 #h #G #L #T2 #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
 #T #T2 #_ #HT2 *
@@ -69,25 +69,25 @@ lemma cpxs_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈*[h] T2 →
 ]
 qed-.
 
-lemma cpxs_inv_lref1: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i ⬈*[h] T2 →
-                      T2 = #(⫯i) ∨
-                      ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ⬈*[h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
+lemma cpxs_inv_lref1: â\88\80h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #â\86\91i ⬈*[h] T2 →
+                      T2 = #(â\86\91i) ∨
+                      ∃∃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 *
 [ #H destruct
   elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
-  * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
-| * #I #K #V1 #T1 #Hi #HT1 #H destruct
+  * /4 width=6 by cpx_cpxs, ex3_3_intro, or_intror/
+| * #I #K #T1 #Hi #HT1 #H destruct
   elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
-  /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/
+  /4 width=6 by cpxs_strap1, drops_refl, drops_drop, ex3_3_intro, or_intror/
 ]
 qed-.
 
 (* Basic_2A1: was: cpxs_inv_lref1 *)
 lemma cpxs_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h] T2 →
                             T2 = #i ∨
-                            â\88\83â\88\83I,K,V1,T1. â¬\87*[i] L â\89¡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h] T1 &
-                                         â¬\86*[⫯i] T1 â\89¡ T2.
+                            â\88\83â\88\83I,K,V1,T1. â¬\87*[i] L â\89\98 K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h] T1 &
+                                         â¬\86*[â\86\91i] T1 â\89\98 T2.
 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
 #T #T2 #_ #HT2 *
 [ #H destruct
@@ -103,17 +103,17 @@ qed-.
 (* Properties with generic relocation ***************************************)
 
 (* Basic_2A1: includes: cpxs_lift *)
-lemma cpxs_lifts_sn: ∀h,G. d_liftable2_sn (cpxs h G).
-/3 width=10 by cpx_lifts_sn, cpxs_strap1, d2_liftable_sn_LTC/ qed-.
+lemma cpxs_lifts_sn: ∀h,G. d_liftable2_sn … lifts (cpxs h G).
+/3 width=10 by cpx_lifts_sn, cpxs_strap1, d2_liftable_sn_CTC/ qed-.
 
-lemma cpxs_lifts_bi: ∀h,G. d_liftable2_bi (cpxs h G).
-/3 width=9 by cpxs_lifts_sn, d_liftable2_sn_bi/ qed-.
+lemma cpxs_lifts_bi: ∀h,G. d_liftable2_bi … lifts (cpxs h G).
+/3 width=12 by cpxs_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.
 
 (* Inversion lemmas with generic relocation *********************************)
 
 (* Basic_2A1: includes: cpxs_inv_lift1 *)
-lemma cpxs_inv_lifts_sn: ∀h,G. d_deliftable2_sn (cpxs h G).
-/3 width=6 by d2_deliftable_sn_LTC, cpx_inv_lifts_sn/ qed-.
+lemma cpxs_inv_lifts_sn: ∀h,G. d_deliftable2_sn … lifts (cpxs h G).
+/3 width=6 by d2_deliftable_sn_CTC, cpx_inv_lifts_sn/ qed-.
 
-lemma cpxs_inv_lifts_bi: ∀h,G. d_deliftable2_bi (cpxs h G).
-/3 width=9 by cpxs_inv_lifts_sn, d_deliftable2_sn_bi/ qed-.
+lemma cpxs_inv_lifts_bi: ∀h,G. d_deliftable2_bi … lifts (cpxs h G).
+/3 width=12 by cpxs_inv_lifts_sn, d_deliftable2_sn_bi, lifts_inj/ qed-.