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/ldrop_ldrop.ma".
16 include "basic_2/unfold/ltpss_ldrop.ma".
17 include "basic_2/unfold/thin.ma".
19 (* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
21 (* Properties on local environment slicing **********************************)
23 lemma thin_ldrop_conf_ge: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
24 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
25 d1 + e1 ≤ e2 → ⇩[0, e2 - e1] L1 ≡ L2.
26 #L0 #L1 #d1 #e1 * /3 width=8 by ltpss_ldrop_conf_ge, ldrop_conf_ge/
29 lemma thin_ldrop_conf_be: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
30 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
31 ∃∃L. ▼*[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L.
32 #L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #Hd1e2 #He2de1
33 elim (ltpss_ldrop_conf_be … HL0 … HL02 ? ?) -L0 // #L0 #HL20 #HL0
34 elim (ldrop_conf_be … HL1 … HL0 ? ?) -L // -Hd1e2 -He2de1 /3 width=3/
37 lemma thin_ldrop_conf_le: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
38 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
39 ∃∃L. ▼*[d1 - e2, e1] L2 ≡ L & ⇩[0, e2] L1 ≡ L.
40 #L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #He2d1
41 elim (ltpss_ldrop_conf_le … HL0 … HL02 ?) -L0 // #L0 #HL20 #HL0
42 elim (ldrop_conf_le … HL1 … HL0 ?) -L // -He2d1 /3 width=3/
45 lemma thin_ldrop_trans_ge: ∀L1,L0,d1,e1. ▼*[d1, e1] L1 ≡ L0 →
46 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
47 d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
48 #L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #Hd1e2
49 lapply (ldrop_trans_ge … HL0 … HL02 ?) -L0 // #HL2
50 lapply (ltpss_ldrop_trans_ge … HL1 … HL2 ?) -L // /2 width=1/
53 lemma thin_ldrop_trans_le: ∀L1,L0,d1,e1. ▼*[d1, e1] L1 ≡ L0 →
54 ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
55 ∃∃L. ▼*[d1 - e2, e1] L ≡ L2 & ⇩[0, e2] L1 ≡ L.
56 #L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #He2d1
57 elim (ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL0 #HL02
58 elim (ltpss_ldrop_trans_le … HL1 … HL0 He2d1) -L -He2d1 /3 width=3/