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 "static_2/relocation/drops_ctc.ma".
16 include "basic_2/rt_transition/cpx_drops.ma".
17 include "basic_2/rt_computation/cpxs.ma".
19 (* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
21 (* Advanced properties ******************************************************)
23 lemma cpxs_delta: ∀h,I,G,K,V1,V2. ❪G,K❫ ⊢ V1 ⬈*[h] V2 →
24 ∀W2. ⇧[1] V2 ≘ W2 → ❪G,K.ⓑ[I]V1❫ ⊢ #0 ⬈*[h] W2.
25 #h #I #G #K #V1 #V2 #H @(cpxs_ind … H) -V2
26 [ /3 width=3 by cpx_cpxs, cpx_delta/
27 | #V #V2 #_ #HV2 #IH #W2 #HVW2
28 elim (lifts_total V (𝐔❨1❩))
29 /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
33 lemma cpxs_lref: ∀h,I,G,K,T,i. ❪G,K❫ ⊢ #i ⬈*[h] T →
34 ∀U. ⇧[1] T ≘ U → ❪G,K.ⓘ[I]❫ ⊢ #↑i ⬈*[h] U.
35 #h #I #G #K #T #i #H @(cpxs_ind … H) -T
36 [ /3 width=3 by cpx_cpxs, cpx_lref/
37 | #T0 #T #_ #HT2 #IH #U #HTU
38 elim (lifts_total T0 (𝐔❨1❩))
39 /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
43 (* Basic_2A1: was: cpxs_delta *)
44 lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.
45 ⇩[i] L ≘ K.ⓑ[I]V1 → ❪G,K❫ ⊢ V1 ⬈*[h] V2 →
46 ∀W2. ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ⬈*[h] W2.
47 #h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
48 [ /3 width=7 by cpx_cpxs, cpx_delta_drops/
49 | #V #V2 #_ #HV2 #IH #W2 #HVW2
50 elim (lifts_total V (𝐔❨↑i❩))
51 /4 width=11 by cpxs_strap1, cpx_lifts_bi, drops_isuni_fwd_drop2/
55 (* Advanced inversion lemmas ************************************************)
57 lemma cpxs_inv_zero1: ∀h,G,L,T2. ❪G,L❫ ⊢ #0 ⬈*[h] T2 →
59 ∃∃I,K,V1,V2. ❪G,K❫ ⊢ V1 ⬈*[h] V2 & ⇧[1] V2 ≘ T2 &
61 #h #G #L #T2 #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
64 elim (cpx_inv_zero1 … HT2) -HT2 /2 width=1 by or_introl/
65 * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
66 | * #I #K #V1 #T1 #HVT1 #HT1 #H destruct
67 elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
68 /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/
72 lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ❪G,L❫ ⊢ #↑i ⬈*[h] T2 →
74 ∃∃I,K,T. ❪G,K❫ ⊢ #i ⬈*[h] T & ⇧[1] T ≘ T2 & L = K.ⓘ[I].
75 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
78 elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
79 * /4 width=6 by cpx_cpxs, ex3_3_intro, or_intror/
80 | * #I #K #T1 #Hi #HT1 #H destruct
81 elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
82 /4 width=6 by cpxs_strap1, drops_refl, drops_drop, ex3_3_intro, or_intror/
86 (* Basic_2A1: was: cpxs_inv_lref1 *)
87 lemma cpxs_inv_lref1_drops: ∀h,G,L,T2,i. ❪G,L❫ ⊢ #i ⬈*[h] T2 →
89 ∃∃I,K,V1,T1. ⇩[i] L ≘ K.ⓑ[I]V1 & ❪G,K❫ ⊢ V1 ⬈*[h] T1 &
91 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
94 elim (cpx_inv_lref1_drops … HT2) -HT2 /2 width=1 by or_introl/
95 * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
96 | * #I #K #V1 #T1 #HLK #HVT1 #HT1
97 lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
98 elim (cpx_inv_lifts_sn … HT2 … H0LK … HT1) -H0LK -T
99 /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/
103 (* Properties with generic relocation ***************************************)
105 (* Basic_2A1: includes: cpxs_lift *)
106 lemma cpxs_lifts_sn: ∀h,G. d_liftable2_sn … lifts (cpxs h G).
107 /3 width=10 by cpx_lifts_sn, cpxs_strap1, d2_liftable_sn_CTC/ qed-.
109 lemma cpxs_lifts_bi: ∀h,G. d_liftable2_bi … lifts (cpxs h G).
110 /3 width=12 by cpxs_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.
112 (* Inversion lemmas with generic relocation *********************************)
114 (* Basic_2A1: includes: cpxs_inv_lift1 *)
115 lemma cpxs_inv_lifts_sn: ∀h,G. d_deliftable2_sn … lifts (cpxs h G).
116 /3 width=6 by d2_deliftable_sn_CTC, cpx_inv_lifts_sn/ qed-.
118 lemma cpxs_inv_lifts_bi: ∀h,G. d_deliftable2_bi … lifts (cpxs h G).
119 /3 width=12 by cpxs_inv_lifts_sn, d_deliftable2_sn_bi, lifts_inj/ qed-.