X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fdelift_alt.ma;h=84c8bee7094c2e0eb4cc239fa004de984cd6fa13;hb=439b6ec33d749ba4e6ae0938e973a85bc23e306e;hp=a53fd9f5dd7253dace4b41daa3d7abc25db46eda;hpb=fc5a0d62ece398d8547dda0f429b9f1e24bca306;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma
index a53fd9f5d..84c8bee70 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma
@@ -14,9 +14,9 @@
 
 include "basic_2/unfold/delift_lift.ma".
 
-(* INVERSE TERM RELOCATION  *************************************************)
+(* INVERSE BASIC TERM RELOCATION  *******************************************)
 
-(* alternative definition of inverse relocation *)
+(* alternative definition of inverse basic term relocation *)
 inductive delifta: nat → nat → lenv → relation term ≝
 | delifta_sort   : ∀L,d,e,k. delifta d e L (⋆k) (⋆k)
 | delifta_lref_lt: ∀L,d,e,i. i < d → delifta d e L (#i) (#i)
@@ -25,30 +25,30 @@ inductive delifta: nat → nat → lenv → relation term ≝
                    ⇧[0, d] V2 ≡ W2 → delifta d e L (#i) W2
 | delifta_lref_ge: ∀L,d,e,i. d + e ≤ i → delifta d e L (#i) (#(i - e))
 | delifta_gref   : ∀L,d,e,p. delifta d e L (§p) (§p)
-| delifta_bind   : ∀L,I,V1,V2,T1,T2,d,e.
+| delifta_bind   : ∀L,a,I,V1,V2,T1,T2,d,e.
                    delifta d e L V1 V2 → delifta (d + 1) e (L. ⓑ{I} V2) T1 T2 →
-                   delifta d e L (ⓑ{I} V1. T1) (ⓑ{I} V2. T2)
+                   delifta d e L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
 | delifta_flat   : ∀L,I,V1,V2,T1,T2,d,e.
                    delifta d e L V1 V2 → delifta d e L T1 T2 →
                    delifta d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
 .
 
-interpretation "inverse relocation (term) alternative"
+interpretation "inverse basic relocation (term) alternative"
    'TSubstAlt L T1 d e T2 = (delifta d e L T1 T2).
 
 (* Basic properties *********************************************************)
 
-lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡≡ T2 →
-                          ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≡≡ T2.
+lemma delifta_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
+                           ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
 [ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+  elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
 | /4 width=1/
 | /3 width=1/
 ]
 qed.
 
-lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e] ≡≡ T2.
+lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼▼*[d, e] T1 ≡ T2.
 #L #T1 @(cw_wf_ind … L T1) -L -T1 #L #T1 elim T1 -T1
 [ * #i #IH #T2 #d #e #H
   [ >(delift_inv_sort1 … H) -H //
@@ -58,12 +58,12 @@ lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e]
     lapply (IH … HV12) // -H /2 width=6/
   | >(delift_inv_gref1 … H) -H //
   ]
-| * #I #V1 #T1 #_ #_ #IH #X #d #e #H
+| * [ #a ] #I #V1 #T1 #_ #_ #IH #X #d #e #H
   [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-    lapply (delift_lsubs_conf … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
+    lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
     lapply (IH … HV12) -HV12 // #HV12
     lapply (IH … HT12) -IH -HT12 /2 width=1/ #HT12
-    lapply (delifta_lsubs_conf … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+    lapply (delifta_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
   | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
     lapply (IH … HV12) -HV12 //
     lapply (IH … HT12) -IH -HT12 // /2 width=1/
@@ -73,7 +73,7 @@ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡≡ T2 → L ⊢ T1 [d, e] ≡ T2.
+lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ ▼▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2.
 #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=1/ /2 width=6/
 qed-. 
 
@@ -81,20 +81,20 @@ lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term.
                       (∀L,d,e,k. R d e L (⋆k) (⋆k)) →
                       (∀L,d,e,i. i < d → R d e L (#i) (#i)) →
                       (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
-                       ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 [O, d + e - i - 1] ≡ V2 →
+                       ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ ▼*[O, d + e - i - 1] V1 ≡ V2 →
                        ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
                       ) →
                       (∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) →
                       (∀L,d,e,p. R d e L (§p) (§p)) →
-                      (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 →
-                       L.ⓑ{I}V2 ⊢ T1 [d + 1, e] ≡ T2 → R d e L V1 V2 →
-                       R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2)
+                      (∀L,a,I,V1,V2,T1,T2,d,e. L ⊢ ▼*[d, e] V1 ≡ V2 →
+                       L.ⓑ{I}V2 ⊢ ▼*[d + 1, e] T1 ≡ T2 → R d e L V1 V2 →
+                       R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
                       ) →
-                      (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 →
-                       L⊢ T1 [d, e] ≡ T2 → R d e L V1 V2 →
+                      (∀L,I,V1,V2,T1,T2,d,e. L ⊢ ▼*[d, e] V1 ≡ V2 →
+                       L⊢ ▼*[d, e] T1 ≡ T2 → R d e L V1 V2 →
                        R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
                       ) →
-                      ∀d,e,L,T1,T2. L ⊢ T1 [d, e] ≡ T2 → R d e L T1 T2.
+                      ∀d,e,L,T1,T2. L ⊢ ▼*[d, e] T1 ≡ T2 → R d e L T1 T2.
 #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #e #L #T1 #T2 #H elim (delift_delifta … H) -L -T1 -T2 -d -e
 // /2 width=1 by delifta_delift/ /3 width=1 by delifta_delift/ /3 width=7 by delifta_delift/
 qed-.