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/relocation/drops_lexs.ma".
16 include "basic_2/s_computation/fqup_weight.ma".
17 include "basic_2/static/frees_drops.ma".
18 include "basic_2/rt_transition/cpx_drops.ma".
20 (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
22 (* Properties with context-sensitive free variables *************************)
24 axiom pippo: āRN,RP,L1,i. ā¬*[ā», šā“iāµ] L1 ā” ā ā
25 āf,L2. L1 ā¦»*[RN, RP, f] L2 ā
26 ā¬*[ā», šā“iāµ] L2 ā” ā.
28 #RN #RP #L1 #i #H1 #f #L2 #H2
29 lapply (lexs_co_dropable_sn ā¦ H1 ā¦ H2) // -HL1 -H2
33 axiom frees_inv_lifts_SO: āb,f,L,U. L ā¢ š
*ā¦Uā¦ ā” f ā
34 āK. ā¬*[b, šā“1āµ] L ā” K ā āT. ā¬*[1] T ā” U ā
35 K ā¢ š
*ā¦Tā¦ ā” ā«±f.
37 axiom frees_pair_flat: āL,T,f1,I1,V1. L.ā{I1}V1 ā¢ š
*ā¦Tā¦ ā” f1 ā
38 āf2,I2,V2. L.ā{I2}V2 ā¢ š
*ā¦Tā¦ ā” f2 ā
39 āf0. f1 ā f2 ā” f0 ā
40 āI0,I. L.ā{I0}ā{I}V1.V2 ā¢ š
*ā¦Tā¦ ā” f0.
42 (* Basic_2A1: was: lpx_cpx_frees_trans *)
43 lemma cpx_frees_trans_lexs: āh,G,L1,T1,f1. L1 ā¢ š
*ā¦T1ā¦ ā” f1 ā
44 āL2. L1 ā¦»*[cpx h G, cfull, f1] L2 ā
45 āT2. ā¦G, L1ā¦ ā¢ T1 ā¬[h] T2 ā
46 āāf2. L2 ā¢ š
*ā¦T2ā¦ ā” f2 & f2 ā f1.
47 #h #G #L1 #T1 @(fqup_wf_ind_eq ā¦ G L1 T1) -G -L1 -T1
48 #G0 #L0 #U0 #IH #G #L1 * *
49 [ -IH #s #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct
50 lapply (frees_inv_sort ā¦ H1) -H1 #Hg1
51 elim (cpx_inv_sort1 ā¦ H0) -H0 #H destruct
52 /3 width=3 by frees_sort_gen, sle_refl, ex2_intro/
53 | #i #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct
54 elim (frees_inv_lref_drops ā¦ H1) -H1 *
56 elim (cpx_inv_lref1_drops ā¦ H0) -H0
57 [ #H destruct lapply (pippo ā¦ HL1 ā¦ H2) -HL1 -H2
58 /3 width=3 by frees_lref_atom, sle_refl, ex2_intro/
59 | * -H2 -Hg1 #I #K1 #V1 #V2 #HLK1
60 lapply (drops_TF ā¦ HLK1) -HLK1 #HLK1
61 lapply (drops_mono ā¦ HLK1 ā¦ HL1) -L1 #H destruct
63 | #f1 #I #K1 #V1 #Hf1 #HLK1 #H destruct
64 elim (cpx_inv_lref1_drops ā¦ H0) -H0
66 elim (lexs_drops_conf_next ā¦ H2 ā¦ HLK1) -H2 [ |*: // ] #K2 #V2 #HLK2 #HK12 #HV12
67 elim (IH ā¦ Hf1 ā¦ HK12 ā¦ HV12) /2 width=2 by fqup_lref/ -L1 -K1 -V1 #f2 #Hf2 #Hf21
68 /4 width=7 by frees_lref_pushs, frees_lref_pair, drops_refl, sle_next, ex2_intro, sle_pushs/
69 | * #J #Y #X #V2 #H #HV12 #HVU2
70 lapply (drops_mono ā¦ H ā¦ HLK1) -H #H destruct
71 elim (lexs_drops_conf_next ā¦ H2 ā¦ HLK1) -H2 [ |*: // ] #K2 #V0 #HLK2 #HK12 #_
72 lapply (drops_isuni_fwd_drop2 ā¦ HLK2) // -V0 #HLK2
73 elim (IH ā¦ Hf1 ā¦ HK12 ā¦ HV12) /2 width=2 by fqup_lref/ -I -L1 -K1 -V1 #f2 #Hf2 #Hf21
74 lapply (frees_lifts ā¦ Hf2 ā¦ HLK2 ā¦ HVU2 ??) /4 width=7 by sle_weak, ex2_intro, sle_pushs/
77 | -IH #l #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct
78 lapply (frees_inv_gref ā¦ H1) -H1 #Hg1
79 lapply (cpx_inv_gref1 ā¦ H0) -H0 #H destruct
80 /3 width=3 by frees_gref_gen, sle_refl, ex2_intro/
81 | #p #I #V1 #T1 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct
82 elim (frees_inv_bind ā¦ H1) -H1 #gV1 #gT1 #HgV1 #HgT1 #Hg1
83 elim (cpx_inv_bind1 ā¦ H0) -H0 *
84 [ #V2 #T2 #HV12 #HT12 #H destruct
85 lapply (sle_lexs_trans ā¦ H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
86 lapply (sle_lexs_trans ā¦ H2 (ā«±gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
87 lapply (lexs_inv_tl ā¦ I ā¦ HL12T ā¦ HV12 ?) // -HL12T #HL12T
88 elim (IH ā¦ HgV1 ā¦ HL12V ā¦ HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
89 elim (IH ā¦ HgT1 ā¦ HL12T ā¦ HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
90 elim (sor_isfin_ex gV2 (ā«±gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/
91 /4 width=10 by frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/
92 | #T2 #HT12 #HUT2 #H0 #H1 destruct -HgV1
93 lapply (sle_lexs_trans ā¦ H2 (ā«±gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
94 lapply (lexs_inv_tl ā¦ Abbr ā¦ V1 V1 HL12T ??) // -HL12T #HL12T
95 elim (IH ā¦ HgT1 ā¦ HL12T ā¦ HT12) // -L1 -T1 #gT2 #HgT2 #HgT21
96 lapply (frees_inv_lifts_SO (ā) ā¦ HgT2 ā¦ L2 ā¦ HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] -V1 -T2
97 /5 width=6 by sor_inv_sle_dx, sle_trans, sle_tl, ex2_intro/
99 | #I #V1 #T0 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct
100 elim (frees_inv_flat ā¦ H1) -H1 #gV1 #gT0 #HgV1 #HgT0 #Hg1
101 elim (cpx_inv_flat1 ā¦ H0) -H0 *
102 [ #V2 #T2 #HV12 #HT12 #H destruct
103 lapply (sle_lexs_trans ā¦ H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
104 lapply (sle_lexs_trans ā¦ H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
105 elim (IH ā¦ HgV1 ā¦ HL12V ā¦ HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
106 elim (IH ā¦ HgT0 ā¦ HL12T ā¦ HT12) // -IH -HgT0 -HL12T -HT12 #gT2 #HgT2 #HgT21
107 elim (sor_isfin_ex gV2 gT2) /2 width=3 by frees_fwd_isfin/
108 /3 width=10 by frees_flat, monotonic_sle_sor, ex2_intro/
109 | #HU2 #H destruct -HgV1
110 lapply (sle_lexs_trans ā¦ H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
111 elim (IH ā¦ HgT0 ā¦ HL12T ā¦ HU2) // -L1 -T0 -V1
112 /4 width=6 by sor_inv_sle_dx, sle_trans, ex2_intro/
113 | #HU2 #H destruct -HgT0
114 lapply (sle_lexs_trans ā¦ H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ -H2 #HL12V
115 elim (IH ā¦ HgV1 ā¦ HL12V ā¦ HU2) // -L1 -T0 -V1
116 /4 width=6 by sor_inv_sle_sn, sle_trans, ex2_intro/
117 | #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H0 #H1 #H destruct
118 elim (frees_inv_bind ā¦ HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0
119 lapply (sle_lexs_trans ā¦ H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
120 lapply (sle_lexs_trans ā¦ H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2
121 lapply (sle_lexs_trans ā¦ H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W
122 lapply (sle_lexs_trans ā¦ H2 (ā«±gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
123 lapply (lexs_inv_tl ā¦ Abst ā¦ HL12T ā¦ HW12 ?) // -HL12T #HL12T
124 elim (IH ā¦ HgV1 ā¦ HL12V ā¦ HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
125 elim (IH ā¦ HgW1 ā¦ HL12W ā¦ HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21
126 elim (IH ā¦ HgT1 ā¦ HL12T ā¦ HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
127 elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H
128 elim (sor_isfin_ex gV0 (ā«±gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
130 [ @(frees_bind ā¦ Hg2) /2 width=5 by frees_flat/ ]
131 | #p #V2 #V #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #H0 #H1 #H destruct
132 elim (frees_inv_bind ā¦ HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0
133 lapply (sle_lexs_trans ā¦ H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
134 lapply (sle_lexs_trans ā¦ H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2
135 lapply (sle_lexs_trans ā¦ H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W
136 lapply (sle_lexs_trans ā¦ H2 (ā«±gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
137 lapply (lexs_inv_tl ā¦ Abbr ā¦ HL12T ā¦ HW12 ?) // -HL12T #HL12T
138 elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_
139 lapply (sor_trans2 ā¦ Hg1 ā¦ HgT0 ā¦ Hg0) -Hg1 -HgT0 #Hg1
140 elim (IH ā¦ HgV1 ā¦ HL12V ā¦ HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
141 elim (IH ā¦ HgW1 ā¦ HL12W ā¦ HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21
142 elim (IH ā¦ HgT1 ā¦ HL12T ā¦ HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
143 elim (sor_isfin_ex (āgV2) gT2) /3 width=3 by frees_fwd_isfin, isfin_push/ #gV0 #HgV0 #H
144 elim (sor_isfin_ex gW2 (ā«±gV0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
145 elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
146 lapply (sor_trans2 ā¦ Hg2 ā¦ (ā«±gT2) ā¦ Hg) /2 width=1 by sor_tl/ #Hg2
147 lapply (frees_lifts (ā) ā¦ HgV2 ā¦ (L2.āW2) ā¦ HV2 ??) [4: |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 #HgV
148 lapply (sor_sym ā¦ Hg) -Hg #Hg
149 /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/
153 lemma cpx_frees_trans: āh,o,G. frees_trans (cpx h o G).
154 /2 width=8 by lpx_cpx_frees_trans/ qed-.
156 lemma lpx_frees_trans: āh,o,G,L1,L2. ā¦G, L1ā¦ ā¢ ā”[h, o] L2 ā
157 āU,i. L2 ā¢ i Ļµ š
*[0]ā¦Uā¦ ā L1 ā¢ i Ļµ š
*[0]ā¦Uā¦.
158 /2 width=8 by lpx_cpx_frees_trans/ qed-.