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/notation/relations/predtysnstrong_5.ma".
16 include "basic_2/static/lfdeq.ma".
17 include "basic_2/rt_transition/lfpx.ma".
19 (* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
21 definition lfsx: ∀h. sd h → relation3 term genv lenv ≝
22 λh,o,T,G. SN … (lfpx h G T) (lfdeq h o T).
25 "strong normalization for uncounted context-sensitive parallel rt-transition on referred entries (local environment)"
26 'PRedTySNStrong h o T G L = (lfsx h o T G L).
28 (* Basic eliminators ********************************************************)
30 (* Basic_2A1: was: lsx_ind *)
31 lemma lfsx_ind: ∀h,o,G,T. ∀R:predicate lenv.
32 (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
33 (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → R L2) →
36 ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
37 #h #o #G #T #R #H0 #L1 #H elim H -L1
38 /5 width=1 by lfdeq_sym, SN_intro/
41 (* Basic properties *********************************************************)
43 (* Basic_2A1: was: lsx_intro *)
44 lemma lfsx_intro: ∀h,o,G,L1,T.
45 (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
46 G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
47 /5 width=1 by lfdeq_sym, SN_intro/ qed.
49 lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄.
50 #h #o #G #L1 #s @lfsx_intro
51 #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H *
53 | #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
57 lemma lfsx_gref: ∀h,o,G,L,l,p. G ⊢ ⬈*[h, o, §p, l] L.
58 #h #o #G #L1 #l #p @lfsx_intro
59 #L2 #HL12 #H elim H -H
60 /3 width=4 by lfpx_fwd_length, lfdeq_gref/
63 (* Basic forward lemmas *****************************************************)
65 lemma lfsx_fwd_bind_sn: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L →
67 #h #o #a #I #G #L #V #T #l #H @(lfsx_ind … H) -L
68 #L1 #_ #IHL1 @lfsx_intro
69 #L2 #HL12 #HV @IHL1 /3 width=4 by lfdeq_fwd_bind_sn/
72 lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
74 #h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
75 #L1 #_ #IHL1 @lfsx_intro
76 #L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/
79 lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
81 #h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
82 #L1 #_ #IHL1 @lfsx_intro
83 #L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/
86 lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L →
88 #h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/
91 (* Basic inversion lemmas ***************************************************)
93 lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
94 G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L.
95 /3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-.
97 (* Basic_2A1: removed theorems 5:
98 lsx_atom lsx_sort lsx_gref lsx_ge_up lsx_ge