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 "ground_2/xoa/ex_4_5.ma".
16 include "basic_2/rt_transition/cpg_drops.ma".
17 include "basic_2/rt_transition/cpx.ma".
19 (* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
21 (* Advanced properties ******************************************************)
23 (* Basic_2A1: was: cpx_delta *)
24 lemma cpx_delta_drops: ∀h,I,G,L,K,V,V2,W2,i.
25 ⇩[i] L ≘ K.ⓑ[I]V → ❪G,K❫ ⊢ V ⬈[h] V2 →
26 ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ⬈[h] W2.
27 #h * #G #L #K #V #V2 #W2 #i #HLK *
28 /3 width=7 by cpg_ell_drops, cpg_delta_drops, ex_intro/
31 (* Advanced inversion lemmas ************************************************)
33 (* Basic_2A1: was: cpx_inv_atom1 *)
34 lemma cpx_inv_atom1_drops: ∀h,I,G,L,T2. ❪G,L❫ ⊢ ⓪[I] ⬈[h] T2 →
36 | ∃∃s. T2 = ⋆(⫯[h]s) & I = Sort s
37 | ∃∃J,K,V,V2,i. ⇩[i] L ≘ K.ⓑ[J]V & ❪G,K❫ ⊢ V ⬈[h] V2 &
38 ⇧[↑i] V2 ≘ T2 & I = LRef i.
39 #h #I #G #L #T2 * #c #H elim (cpg_inv_atom1_drops … H) -H *
40 /4 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex2_intro, ex_intro/
43 (* Basic_2A1: was: cpx_inv_lref1 *)
44 lemma cpx_inv_lref1_drops: ∀h,G,L,T2,i. ❪G,L❫ ⊢ #i ⬈[h] T2 →
46 ∃∃J,K,V,V2. ⇩[i] L ≘ K. ⓑ[J]V & ❪G,K❫ ⊢ V ⬈[h] V2 &
48 #h #G #L #T1 #i * #c #H elim (cpg_inv_lref1_drops … H) -H *
49 /4 width=7 by ex3_4_intro, ex_intro, or_introl, or_intror/
52 (* Properties with generic slicing for local environments *******************)
54 (* Basic_2A1: includes: cpx_lift *)
55 lemma cpx_lifts_sn: ∀h,G. d_liftable2_sn … lifts (cpx h G).
56 #h #G #K #T1 #T2 * #cT #HT12 #b #f #L #HLK #U1 #HTU1
57 elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
58 /3 width=4 by ex2_intro, ex_intro/
61 lemma cpx_lifts_bi: ∀h,G. d_liftable2_bi … lifts (cpx h G).
62 #h #G #K #T1 #T2 * /3 width=10 by cpg_lifts_bi, ex_intro/
65 (* Inversion lemmas with generic slicing for local environments *************)
67 (* Basic_2A1: includes: cpx_inv_lift1 *)
68 lemma cpx_inv_lifts_sn: ∀h,G. d_deliftable2_sn … lifts (cpx h G).
69 #h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1
70 elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
71 /3 width=4 by ex2_intro, ex_intro/
74 lemma cpx_inv_lifts_bi: ∀h,G. d_deliftable2_bi …lifts (cpx h G).
75 #h #G #L #U1 #U2 * /3 width=10 by cpg_inv_lifts_bi, ex_intro/