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 (* Basic_2A1: was: lsx_sort *)
50 lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄.
51 #h #o #G #L1 #s @lfsx_intro
52 #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H *
54 | #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
55 /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort_gen, frees_inv_sort/
59 (* Basic_2A1: was: lsx_gref *)
60 lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄.
61 #h #o #G #L1 #s @lfsx_intro
62 #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_gref … H) -H *
64 | #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
65 /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref_gen, frees_inv_gref/
69 (* Basic_2A1: removed theorems 2: