]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / rsx.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "basic_2/notation/relations/predtysnstrong_3.ma".
16 include "static_2/static/reqx.ma".
17 include "basic_2/rt_transition/lpx.ma".
18
19 (* STRONGLY NORMALIZING REFERRED LOCAL ENVS FOR EXTENDED RT-TRANSITION ******)
20
21 definition rsx (G) (T): predicate lenv ≝
22            SN … (lpx G) (λL1,L2. L1 ≅[T] L2).
23
24 interpretation
25   "strong normalization for extended context-sensitive parallel rt-transition on referred entries (local environment)"
26   'PRedTySNStrong G T L = (rsx G T L).
27
28 (* Basic eliminators ********************************************************)
29
30 (* Basic_2A1: uses: lsx_ind *)
31 lemma rsx_ind (G) (T) (Q:predicate …):
32       (∀L1. G ⊢ ⬈*𝐒[T] L1 →
33         (∀L2. ❪G,L1❫ ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → Q L2) →
34         Q L1
35       ) →
36       ∀L. G ⊢ ⬈*𝐒[T] L →  Q L.
37 #G #T #Q #H0 #L1 #H elim H -L1
38 /5 width=1 by SN_intro/
39 qed-.
40
41 (* Basic properties *********************************************************)
42
43 (* Basic_2A1: uses: lsx_intro *)
44 lemma rsx_intro (G) (T):
45       ∀L1.
46       (∀L2. ❪G,L1❫ ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → G ⊢ ⬈*𝐒[T] L2) →
47       G ⊢ ⬈*𝐒[T] L1.
48 /5 width=1 by SN_intro/ qed.
49
50 (* Basic forward lemmas *****************************************************)
51
52 (* Basic_2A1: uses: lsx_fwd_pair_sn lsx_fwd_bind_sn lsx_fwd_flat_sn *)
53 lemma rsx_fwd_pair_sn (G):
54       ∀I,L,V,T. G ⊢ ⬈*𝐒[②[I]V.T] L →
55       G ⊢ ⬈*𝐒[V] L.
56 #G #I #L #V #T #H
57 @(rsx_ind … H) -L #L1 #_ #IHL1
58 @rsx_intro #L2 #HL12 #HnL12
59 /4 width=3 by reqg_fwd_pair_sn/
60 qed-.
61
62 (* Basic_2A1: uses: lsx_fwd_flat_dx *)
63 lemma rsx_fwd_flat_dx (G):
64       ∀I,L,V,T. G ⊢ ⬈*𝐒[ⓕ[I]V.T] L →
65       G ⊢ ⬈*𝐒[T] L.
66 #G #I #L #V #T #H
67 @(rsx_ind … H) -L #L1 #_ #IHL1
68 @rsx_intro #L2 #HL12 #HnL12
69 /4 width=3 by reqg_fwd_flat_dx/
70 qed-.
71
72 fact rsx_fwd_pair_aux (G):
73      ∀L. G ⊢ ⬈*𝐒[#0] L →
74      ∀I,K,V. L = K.ⓑ[I]V → G ⊢ ⬈*𝐒[V] K.
75 #G #L #H
76 @(rsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct
77 /5 width=5 by lpx_pair, rsx_intro, reqg_fwd_zero_pair/
78 qed-.
79
80 lemma rsx_fwd_pair (G):
81       ∀I,K,V. G ⊢ ⬈*𝐒[#0] K.ⓑ[I]V → G ⊢ ⬈*𝐒[V] K.
82 /2 width=4 by rsx_fwd_pair_aux/ qed-.
83
84 (* Basic inversion lemmas ***************************************************)
85
86 (* Basic_2A1: uses: lsx_inv_flat *)
87 lemma rsx_inv_flat (G):
88       ∀I,L,V,T. G ⊢ ⬈*𝐒[ⓕ[I]V.T] L →
89       ∧∧ G ⊢ ⬈*𝐒[V] L & G ⊢ ⬈*𝐒[T] L.
90 /3 width=3 by rsx_fwd_pair_sn, rsx_fwd_flat_dx, conj/ qed-.
91
92 (* Basic_2A1: removed theorems 9:
93               lsx_ge_up lsx_ge
94               lsxa_ind lsxa_intro lsxa_lleq_trans lsxa_lpxs_trans lsxa_intro_lpx lsx_lsxa lsxa_inv_lsx
95 *)