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/grammar/lpx_sn.ma".
16 include "basic_2/relocation/ldrop.ma".
18 (* DROPPING *****************************************************************)
20 (* Properties on sn pointwise extension *************************************)
22 lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R).
23 #R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
24 [ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
25 /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
26 | #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
27 #L2 #V2 #HL12 #HV12 #H destruct
28 /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
29 | #I #L1 #K1 #V1 #e #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H
30 #L2 #V2 #HL12 #HV12 #H destruct
31 elim (IHLK1 … HL12) -L1 /3 width=3 by ldrop_drop, ex2_intro/
32 | #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
33 elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
34 elim (HR … HV12 … HLK1 … HWV1) -V1
35 elim (IHLK1 … HL12) -L1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/
39 lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
40 l_liftable R → dedropable_sn (lpx_sn R).
41 #R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
42 [ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
43 /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
44 | #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
45 #K2 #V2 #HK12 #HV12 #H destruct
46 /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
47 | #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1
48 /3 width=5 by ldrop_drop, lpx_sn_pair, ex2_intro/
49 | #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
50 elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
51 elim (lift_total W2 d e) #V2 #HWV2
52 lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1
53 elim (IHLK1 … HK12) -K1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/
57 fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⇩[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
58 d = 0 → ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2.
59 #R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e
60 [ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H
61 /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
62 | #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H
63 #K1 #V1 #HK12 #HV12 #H destruct
64 /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
65 | #I #L2 #K2 #V2 #e #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H
66 #L1 #V1 #HL12 #HV12 #H destruct
67 elim (IHLK2 … HL12) -L2 /3 width=3 by ldrop_drop, ex2_intro/
68 | #I #L2 #K2 #V2 #W2 #d #e #_ #_ #_ #L1 #_
69 <plus_n_Sm #H destruct
73 lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R).
74 /2 width=5 by lpx_sn_dropable_aux/ qed-.