X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fsubstitution%2Ftps.ma;h=d284060f1b1cd3f814017a2f66322e6a015db853;hb=ea83c19f4cac864dd87eb059d8aeb2343eba480f;hp=f60641afcdd46056337a2287285cc22c5dff5101;hpb=78d4844bcccb3deb58a3179151c3045298782b18;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
index f60641afc..d284060f1 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
@@ -34,12 +34,12 @@ interpretation "parallel substritution (term)"
 
 (* Basic properties *********************************************************)
 
-lemma tps_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
-                      ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▶ [d, e] T2.
+lemma tps_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶ [d, e] T2 →
+                       ∀L2. L2 ≼ [d, e] L1 → L2 ⊢ T1 ▶ [d, e] T2.
 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
 [ //
 | #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
-  elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/
+  elim (ldrop_lsubs_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /2 width=4/
 | /4 width=1/
 | /3 width=1/
 ]
@@ -115,7 +115,30 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ∀i. d ≤ i →
   elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
   elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
   -Hdi -Hide >arith_c1x #T #HT1 #HT2
-  lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
+  elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
+  -Hdi -Hide /3 width=5/
+]
+qed.
+
+lemma tps_split_down: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 →
+                      ∀i. d ≤ i → i ≤ d + e →
+                      ∃∃T. L ⊢ T1 ▶ [i, d + e - i] T &
+                           L ⊢ T ▶ [d, i - d] T2.
+#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
+[ /2 width=3/
+| #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
+  elim (lt_or_ge i j)
+  [ -Hide -Hjde >(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /4 width=4/
+  | -Hdi -Hdj
+    >(plus_minus_m_m (d+e) j) in Hide; // -Hjde /3 width=4/
+  ]
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
+  elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
+  elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
+  -Hdi -Hide >arith_c1x #T #HT1 #HT2
+  lapply (tps_lsubs_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
   elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
   -Hdi -Hide /3 width=5/