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/ynat/ynat_max.ma".
16 include "basic_2/computation/lsx_drop.ma".
17 include "basic_2/computation/lsx_lpx.ma".
18 include "basic_2/computation/lsx_lpxs.ma".
19 include "basic_2/computation/lcosx.ma".
21 (* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
23 (* Properties on extended context-sensitive parallel reduction for term *****)
25 lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
26 ∀l. G ⊢ ~⬊*[h, g, l] L →
27 G ⊢ ⬊*[h, g, T1, l] L → G ⊢ ⬊*[h, g, T2, l] L.
28 #h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
29 [ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #l #HL #H
30 elim (ylt_split i l) #Hli [ -H | -HL ]
31 [ <(ymax_pre_sn l (⫯i)) /2 width=1 by ylt_fwd_le_succ1/
32 elim (lcosx_drop_trans_lt … HL … HLK) // -HL -Hli
33 lapply (drop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
34 | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hli
35 lapply (drop_fwd_drop2 … HLK) -HLK
36 /4 width=10 by lsx_ge, lsx_lift_le/
38 | #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
39 elim (lsx_inv_bind … H) -H #HV1 #HT1
40 @lsx_bind /2 width=2 by/ (**) (* explicit constructor *)
41 @(lsx_lreq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, lreq_succ/
42 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
43 elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/
44 | #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #l #HL #H
45 elim (lsx_inv_bind … H) -H #HV #HU1
46 <(ypred_succ l) <yminus_SO2
47 /4 width=7 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
48 | #G #L #V #T1 #T2 #_ #IHT12 #l #HL #H
49 elim (lsx_inv_flat … H) -H /2 width=1 by/
50 | #G #L #V1 #V2 #T #_ #IHV12 #l #HL #H
51 elim (lsx_inv_flat … H) -H /2 width=1 by/
52 | #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #l #HL #H
53 elim (lsx_inv_flat … H) -H #HV1 #H
54 elim (lsx_inv_bind … H) -H #HW1 #HT1
55 @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *)
56 @(lsx_lreq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, lreq_succ/
57 | #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #l #HL #H
58 elim (lsx_inv_flat … H) -H #HV1 #H
59 elim (lsx_inv_bind … H) -H #HW1 #HT1
60 @lsx_bind /2 width=1 by/ (**) (* explicit constructor *)
61 @lsx_flat [ <yplus_SO2 /3 width=7 by lsx_lift_ge, drop_drop/ ]
62 @(lsx_lreq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, lreq_succ/
66 lemma lsx_cpx_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
67 G ⊢ ⬊*[h, g, T1, 0] L → G ⊢ ⬊*[h, g, T2, 0] L.
68 /2 width=3 by lsx_cpx_trans_lcosx/ qed-.