X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Ftpss_lift.ma;h=a68f86e32bfafd063900f7e0ad66ec63fe546d90;hb=eae50cc815292d335df1c488a00b39ef98fa5870;hp=f12e38877fec2e4d963bef8eb5dc0cc5d531e7ba;hpb=a8c166f1e1baeeae04553058bd179420ada8bbe7;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma
index f12e38877..a68f86e32 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma
@@ -21,8 +21,8 @@ include "basic_2/unfold/tpss.ma".
 
 lemma tpss_subst: ∀L,K,V,U1,i,d,e.
                   d ≤ i → i < d + e →
-                  ⇩[0, i] L ≡ K. ⓓV → K ⊢ V [0, d + e - i - 1] ▶* U1 →
-                  ∀U2. ⇧[0, i + 1] U1 ≡ U2 → L ⊢ #i [d, e] ▶* U2.
+                  ⇩[0, i] L ≡ K. ⓓV → K ⊢ V ▶* [0, d + e - i - 1] U1 →
+                  ∀U2. ⇧[0, i + 1] U1 ≡ U2 → L ⊢ #i ▶* [d, e] U2.
 #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
 [ /3 width=4/
 | #U #U1 #_ #HU1 #IHU #U2 #HU12
@@ -36,11 +36,11 @@ qed.
 
 (* Advanced inverion lemmas *************************************************)
 
-lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶* T2 →
+lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} ▶* [d, e] T2 →
                       T2 = ⓪{I} ∨
                       ∃∃K,V1,V2,i. d ≤ i & i < d + e &
                                    ⇩[O, i] L ≡ K. ⓓV1 &
-                                   K ⊢ V1 [0, d + e - i - 1] ▶* V2 &
+                                   K ⊢ V1 ▶* [0, d + e - i - 1] V2 &
                                    ⇧[O, i + 1] V2 ≡ T2 &
                                    I = LRef i.
 #L #T2 #I #d #e #H @(tpss_ind … H) -T2
@@ -50,24 +50,31 @@ lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶* T2 →
     elim (tps_inv_atom1 … HT2) -HT2 [ /2 width=1/ | * /3 width=10/ ]
   | * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
     lapply (ldrop_fwd_ldrop2 … HLK) #H
-    elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
+    elim (tps_inv_lift1_ge_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
     @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2 width=3/ (**) (* /4 width=10/ is too slow *)
   ]
 ]
 qed-.
 
-lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ▶* T2 →
+lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i ▶* [d, e] T2 →
                       T2 = #i ∨
                       ∃∃K,V1,V2. d ≤ i & i < d + e &
                                  ⇩[O, i] L ≡ K. ⓓV1 &
-                                 K ⊢ V1 [0, d + e - i - 1] ▶* V2 &
+                                 K ⊢ V1 ▶* [0, d + e - i - 1] V2 &
                                  ⇧[O, i + 1] V2 ≡ T2.
 #L #T2 #i #d #e #H
 elim (tpss_inv_atom1 … H) -H /2 width=1/
 * #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/
 qed-.
 
-lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶* T2 →
+lemma tpss_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e + 1] T2 →
+                   ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 ▶* [d + 1, e] T2.
+#L #T1 #T2 #d #e #H #K #V #HLK @(tpss_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT
+lapply (tps_inv_S2 … HT2 … HLK) -HT2 -HLK /2 width=3/
+qed-.
+
+lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 1] T2 →
                          ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
 #L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
 #T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
@@ -75,10 +82,10 @@ qed-.
 
 (* Relocation properties ****************************************************)
 
-lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
+lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 →
                     ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
                     ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
-                    L ⊢ U1 [dt, et] ▶* U2.
+                    L ⊢ U1 ▶* [dt, et] U2.
 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
@@ -88,10 +95,10 @@ lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
 ]
 qed.
 
-lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
+lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 →
                     ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
                     ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
-                    ∀U2. ⇧[d, e] T2 ≡ U2 → L ⊢ U1 [dt, et + e] ▶* U2.
+                    ∀U2. ⇧[d, e] T2 ≡ U2 → L ⊢ U1 ▶* [dt, et + e] U2.
 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
@@ -101,10 +108,10 @@ lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
 ]
 qed.
 
-lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
+lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 →
                     ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K →
                     ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
-                    L ⊢ U1 [dt + e, et] ▶* U2.
+                    L ⊢ U1 ▶* [dt + e, et] U2.
 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
@@ -114,10 +121,10 @@ lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
 ]
 qed.
 
-lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
                          ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
                          dt + et ≤ d →
-                         ∃∃T2. K ⊢ T1 [dt, et] ▶* T2 & ⇧[d, e] T2 ≡ U2.
+                         ∃∃T2. K ⊢ T1 ▶* [dt, et] T2 & ⇧[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2
 [ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -125,10 +132,10 @@ lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
 ]
 qed.
 
-lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
                          ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
                          dt ≤ d → d + e ≤ dt + et →
-                         ∃∃T2. K ⊢ T1 [dt, et - e] ▶* T2 & ⇧[d, e] T2 ≡ U2.
+                         ∃∃T2. K ⊢ T1 ▶* [dt, et - e] T2 & ⇧[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2
 [ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -136,10 +143,10 @@ lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
 ]
 qed.
 
-lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
                          ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
                          d + e ≤ dt →
-                         ∃∃T2. K ⊢ T1 [dt - e, et] ▶* T2 & ⇧[d, e] T2 ≡ U2.
+                         ∃∃T2. K ⊢ T1 ▶* [dt - e, et] T2 & ⇧[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2
 [ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -148,19 +155,42 @@ lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
 qed.
 
 lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
-                         L ⊢ U1 [d, e] ▶* U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
+                         L ⊢ U1 ▶* [d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
 #L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 //
 #U #U2 #_ #HU2 #IHU destruct
 <(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
 qed.
 
-lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ▶* U2 →
+lemma tpss_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
+                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                            d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
+                            ∃∃T2. K ⊢ T1 ▶* [d, dt + et - (d + e)] T2 &
+                                 ⇧[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(tpss_ind … H) -U2
+[ /2 width=3/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (tps_inv_lift1_ge_up … HU2 … HLK … HTU ? ? ?) -HU2 -HLK -HTU // /3 width=3/
+]
+qed.
+
+lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
                             ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
                             dt ≤ d → dt + et ≤ d + e →
-                            ∃∃T2. K ⊢ T1 [dt, d - dt] ▶* T2 & ⇧[d, e] T2 ≡ U2.
+                            ∃∃T2. K ⊢ T1 ▶* [dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2
 [ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
   elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
 ]
 qed.
+
+lemma tpss_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
+                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                            dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
+                            ∃∃T2. K ⊢ T1 ▶* [dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(tpss_ind … H) -U2
+[ /2 width=3/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (tps_inv_lift1_le_up … HU2 … HLK … HTU ? ? ?) -HU2 -HLK -HTU // /3 width=3/
+]
+qed.