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/rt_transition/cpm_drops.ma".
17 (* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
19 (* Advanced inversion lemmas ************************************************)
21 (* Basic_2A1: includes: cpr_inv_atom1 *)
22 lemma cpr_inv_atom1_drops: ∀h,I,G,L,T2. ❨G,L❩ ⊢ ⓪[I] ➡[h,0] T2 →
24 | ∃∃K,V,V2,i. ⇩[i] L ≘ K.ⓓV & ❨G,K❩ ⊢ V ➡[h,0] V2 &
25 ⇧[↑i] V2 ≘ T2 & I = LRef i.
26 #h #I #G #L #T2 #H elim (cpm_inv_atom1_drops … H) -H *
27 [ /2 width=1 by or_introl/
28 | #s #_ #_ #H destruct
29 | /3 width=8 by ex4_4_intro, or_intror/
30 | #m #K #V1 #V2 #i #_ #_ #_ #_ #H destruct
34 (* Basic_1: includes: pr0_gen_lref pr2_gen_lref *)
35 (* Basic_2A1: includes: cpr_inv_lref1 *)
36 lemma cpr_inv_lref1_drops: ∀h,G,L,T2,i. ❨G,L❩ ⊢ #i ➡[h,0] T2 →
38 | ∃∃K,V,V2. ⇩[i] L ≘ K. ⓓV & ❨G,K❩ ⊢ V ➡[h,0] V2 &
40 #h #G #L #T2 #i #H elim (cpm_inv_lref1_drops … H) -H *
41 [ /2 width=1 by or_introl/
42 | /3 width=6 by ex3_3_intro, or_intror/
43 | #m #K #V1 #V2 #_ #_ #_ #H destruct