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/syntax/term_vector.ma".
16 include "basic_2/rt_computation/csx.ma".
18 (* STRONGLY NORMALIZING TERMS VECTORS FOR UNBOUND PARALLEL RT-TRANSITION ****)
20 definition csxv (h) (G) (L): predicate (list term) ≝
24 "strong normalization for unbound context-sensitive parallel rt-transition (term vector)"
25 'PRedTyStrong h G L Ts = (csxv h G L Ts).
27 (* Basic inversion lemmas ***************************************************)
29 lemma csxv_inv_cons (h) (G) (L):
30 ∀T,Ts. ❪G,L❫ ⊢ ⬈*𝐒[h] T⨮Ts →
31 ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] T & ❪G,L❫ ⊢ ⬈*𝐒[h] Ts.
34 (* Basic forward lemmas *****************************************************)
36 lemma csx_fwd_applv (h) (G) (L):
37 ∀T,Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.T →
38 ∧∧ ❪G,L❫ ⊢ ⬈*𝐒[h] Vs & ❪G,L❫ ⊢ ⬈*𝐒[h] T.
39 #h #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/
41 lapply (csx_fwd_pair_sn … HVs) #HV
42 lapply (csx_fwd_flat_dx … HVs) -HVs #HVs
43 elim (IHVs HVs) -IHVs -HVs /3 width=1 by conj/