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.ma".
16 include "basic_2/rt_computation/jsx.ma".
18 (* COMPATIBILITY OF STRONG NORMALIZATION FOR EXTENDED RT-TRANSITION *********)
20 (* Forward lemmas with uniform slicing for local environments ***************)
22 lemma jsx_fwd_drops_atom_sn (b) (G):
24 ∀f. 𝐔❪f❫ → ⇩*[b,f]L1 ≘ ⋆ → ⇩*[b,f]L2 ≘ ⋆.
25 #b #G #L1 #L2 #H elim H -L1 -L2
27 | #I #K1 #K2 #_ #IH #f #Hf #H
28 | #I #K1 #K2 #V #_ #HV #IH #f #Hf #H
30 elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ]
32 |2,4: #g #Hg #HK1 #H destruct /3 width=1 by drops_drop/
36 lemma jsx_fwd_drops_unit_sn (b) (G):
38 ∀f. 𝐔❪f❫ → ∀I,K1. ⇩*[b,f]L1 ≘ K1.ⓤ[I] →
39 ∃∃K2. G ⊢ K1 ⊒ K2 & ⇩*[b,f]L2 ≘ K2.ⓤ[I].
40 #b #G #L1 #L2 #H elim H -L1 -L2
42 lapply (drops_inv_atom1 … H) -H * #H #_ destruct
43 | #I #K1 #K2 #HK12 #IH #f #Hf #J #Y1 #H
44 | #I #K1 #K2 #V #HK12 #HV #IH #f #Hf #J #Y1 #H
46 elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ]
47 [1,3: #Hf #H destruct -IH /3 width=3 by drops_refl, ex2_intro/
49 #g #Hg #HK1 #H destruct
50 elim (IH … Hg … HK1) -K1 -Hg #Y2 #HY12 #HKY2
51 /3 width=3 by drops_drop, ex2_intro/
55 lemma jsx_fwd_drops_pair_sn (b) (G):
57 ∀f. 𝐔❪f❫ → ∀I,K1,V. ⇩*[b,f]L1 ≘ K1.ⓑ[I]V →
58 ∨∨ ∃∃K2. G ⊢ K1 ⊒ K2 & ⇩*[b,f]L2 ≘ K2.ⓑ[I]V
59 | ∃∃K2. G ⊢ K1 ⊒ K2 & ⇩*[b,f]L2 ≘ K2.ⓧ & G ⊢ ⬈*𝐒[V] K2.
60 #b #G #L1 #L2 #H elim H -L1 -L2
62 lapply (drops_inv_atom1 … H) -H * #H #_ destruct
63 | #I #K1 #K2 #HK12 #IH #f #Hf #J #Y1 #X1 #H
64 | #I #K1 #K2 #V #HK12 #HV #IH #f #Hf #J #Y1 #X1 #H
66 elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ]
69 /4 width=4 by drops_refl, ex3_intro, ex2_intro, or_introl, or_intror/
71 #g #Hg #HK1 #H destruct
72 elim (IH … Hg … HK1) -K1 -Hg * #Y2 #HY12 #HKY2 [2,4: #HX1 ]
73 /4 width=4 by drops_drop, ex3_intro, ex2_intro, or_introl, or_intror/