1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "Basic-2/substitution/tps_lift.ma".
16 include "Basic-2/substitution/ltps_drop.ma".
18 (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
20 lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
21 ∀L1,d1,e1. L0 [d1, e1] ≫ L1 → d1 + e1 ≤ d2 →
22 L1 ⊢ T2 [d2, e2] ≫ U2.
23 #L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2
25 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
26 lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
27 lapply (ltps_drop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /2/
28 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
29 @tps_bind [ /2/ | @IHTU2 [3: /2/ |1,2: skip | /2/ ] ] (**) (* /3/ is too slow *)
34 lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
35 ∀L1,d1,e1. L0 [d1, e1] ≫ L1 →
36 ∃∃T. L1 ⊢ T2 [d2, e2] ≫ T &
38 #L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2
40 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
41 elim (lt_or_ge i2 d1) #Hi2d1
42 [ elim (ltps_drop_conf_le … HL01 … HLK0 ?) -HL01 HLK0 /2/ #X #H #HLK1
43 elim (ltps_inv_tps11 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
44 lapply (drop_fwd_drop2 … HLK1) #H
45 elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
46 lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -H HV01 HVW0 // >arith_a2 /3/
47 | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
48 [ elim (ltps_drop_conf_be … HL01 … HLK0 ? ?) -HL01 HLK0 [2,3: /2/ ] #X #H #HLK1
49 elim (ltps_inv_tps21 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
50 lapply (drop_fwd_drop2 … HLK1) #H
51 elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
52 lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -H HV01 HVW0 // normalize #HW01
53 lapply (tps_weak … HW01 d1 e1 ? ?) [2,3: /3/ ] >arith_i2 //
54 | lapply (ltps_drop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /3/
57 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
58 elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
59 elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 [2: /2/ ] -HL01 /3 width=5/
60 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
61 elim (IHVW2 … HL01) -IHVW2;
62 elim (IHTU2 … HL01) -IHTU2 HL01 /3 width=5/
66 lemma ltps_tps_trans: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
67 (u1,u:?; i:?) (subst0 i u u1 u2) ->
68 (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).