(* *)
(**************************************************************************)
-(* STRONGLY NORMALIZING TERM VECTORS FOR UNBOUND PARALLEL RT-TRANSITION *****)
-
include "basic_2/rt_computation/cpxs_teqo_vector.ma".
include "basic_2/rt_computation/csx_simple_teqo.ma".
include "basic_2/rt_computation/csx_cnx.ma".
include "basic_2/rt_computation/csx_cpxs.ma".
include "basic_2/rt_computation/csx_vector.ma".
-(* Properties with normal terms for unbound parallel rt-transition **********)
+(* STRONGLY NORMALIZING TERM VECTORS FOR EXTENDED PARALLEL RT-TRANSITION ****)
+
+(* Properties with normal terms for extended parallel rt-transition *********)
(* Basic_1: was just: sn3_appls_lref *)
-lemma csx_applv_cnx (h) (G) (L):
- ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈𝐍[h] T →
- ∀Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] Vs → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.T.
-#h #G #L #T #H1T #H2T #Vs elim Vs -Vs
-[ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/
+lemma csx_applv_cnx (G) (L):
+ ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈𝐍 T →
+ ∀Vs. ❪G,L❫ ⊢ ⬈*𝐒 Vs → ❪G,L❫ ⊢ ⬈*𝐒 ⒶVs.T.
+#G #L #T #H1T #H2T #Vs elim Vs -Vs
+[ #_ normalize in ⊢ (???%); /2 width=1 by cnx_csx/
| #V #Vs #IHV #H
elim (csxv_inv_cons … H) -H #HV #HVs
@csx_appl_simple_teqo /2 width=1 by applv_simple/ -IHV -HV -HVs
(* Advanced properties ******************************************************)
(* Note: strong normalization does not depend on this any more *)
-lemma csx_applv_sort (h) (G) (L):
- ∀s,Vs. ❪G,L❫ ⊢ ⬈*𝐒[h] Vs → ❪G,L❫ ⊢ ⬈*𝐒[h] ⒶVs.⋆s.
+lemma csx_applv_sort (G) (L):
+ ∀s,Vs. ❪G,L❫ ⊢ ⬈*𝐒 Vs → ❪G,L❫ ⊢ ⬈*𝐒 ⒶVs.⋆s.
/3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ qed.