From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 3 Apr 2017 21:31:19 +0000 (+0000)
Subject: - lfsx started ...
X-Git-Tag: make_still_working~465
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5224d5d0ff327a2360c9acd282af66ceed8788fc

- lfsx started ...
- advances to complete csx_aaa
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc
new file mode 100644
index 000000000..fb7dad498
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/gcp_aaa.ma".
+include "basic_2/rt_computation/cpxs_aaa.ma".
+include "basic_2/rt_computation/csx_gcp.ma".
+include "basic_2/rt_computation/csx_gcr.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+
+(* Main properties with atomic arity assignment *****************************)
+
+theorem aaa_csx: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+#h #o #G #L #T #A #H
+@(gcr_aaa … (csx_gcp h o) (csx_gcr h o) … H)
+qed.
+
+(* Advanced eliminators *****************************************************)
+
+fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term.
+                      (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
+                            (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
+                      ) →
+                      ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
+#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
+qed-.
+
+lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term.
+                   (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
+                         (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
+                   ) →
+                   ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
+/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-.
+
+fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term.
+                           (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
+                                 (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
+                           ) →
+                           ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
+#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
+qed-.
+
+(* Basic_2A1: was: aaa_ind_csx_alt *)
+lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term.
+                        (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
+                              (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
+                        ) →
+                        ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
+/5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma
new file mode 100644
index 000000000..ea068dd8d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstrong_5.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( G ⊢ ⬈ * [ break term 46 h , break term 46 o , break term 46 T ] 𝐒 ⦃ break term 46 L ⦄ )"
+   non associative with precedence 45
+   for @{ 'PRedTySNStrong $h $o $T $G $L }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma
deleted file mode 100644
index 14f27aab0..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( G ⊢ ⬊ * [ break term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )"
-   non associative with precedence 45
-   for @{ 'SN $h $o $T $f $G $L }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma
deleted file mode 100644
index ce52c4ca3..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( G ⊢ ⬊ ⬊ * [ break term 46 h , break term 46 o , break term 46 T , break term 46 f ] break term 46 L )"
-   non associative with precedence 45
-   for @{ 'SNAlt $h $o $T $f $G $L }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
index 4e0c82132..9c009bbf2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
@@ -206,6 +206,17 @@ lemma lexs_co: ∀RN1,RP1,RN2,RP2.
 /3 width=1 by lexs_atom, lexs_next, lexs_push/
 qed-.
 
+lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2.
+                    (∀L1,T1,T2. RP1 L1 T1 T2 → RP2 L1 T1 T2) →
+                    ∀f,L1,L2. L1 ⦻*[RN1, RP1, f] L2 → 𝐈⦃f⦄ →
+                    L1 ⦻*[RN2, RP2, f] L2.
+#RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
+#f #I #K1 #K2 #V1 #V2 #_ #HV12 #IH #H
+[ elim (isid_inv_next … H) -H //
+| /4 width=3 by lexs_push, isid_inv_push/
+] 
+qed-.
+
 lemma sle_lexs_trans: ∀RN,RP. (∀L,T1,T2. RN L T1 T2 → RP L T1 T2) →
                       ∀f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 →
                       ∀f1. f1 ⊆ f2 → L1 ⦻*[RN, RP, f1] L2.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma
new file mode 100644
index 000000000..2266edbad
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_aaa.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reduction/lpx_aaa.ma".
+include "basic_2/computation/cpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma cpxs_aaa_conf: ∀h,o,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
+                     ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+#h #o #G #L #T1 #A #HT1 #T2 #HT12
+@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by cpx_aaa_conf/
+qed-.
+
+lemma cprs_aaa_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+/3 width=5 by cpxs_aaa_conf, cprs_cpxs/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma
index 2266edbad..3fa11c673 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma
@@ -12,18 +12,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpx_aaa.ma".
-include "basic_2/computation/cpxs.ma".
+include "basic_2/rt_transition/lfpx_aaa.ma".
+include "basic_2/rt_computation/cpxs.ma".
 
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
 
-(* Properties about atomic arity assignment on terms ************************)
+(* Properties with atomic arity assignment on terms *************************)
 
-lemma cpxs_aaa_conf: ∀h,o,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                     ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-#h #o #G #L #T1 #A #HT1 #T2 #HT12
+lemma cpxs_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
+                     ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+#h #G #L #T1 #A #HT1 #T2 #HT12
 @(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=5 by cpx_aaa_conf/
 qed-.
-
-lemma cprs_aaa_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
-/3 width=5 by cpxs_aaa_conf, cprs_cpxs/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma
deleted file mode 100644
index 89f226a30..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma
+++ /dev/null
@@ -1,58 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/computation/gcp_aaa.ma".
-include "basic_2/computation/cpxs_aaa.ma".
-include "basic_2/computation/csx_theq_vector.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-
-(* Main properties on atomic arity assignment *******************************)
-
-theorem aaa_csx: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, o] T.
-#h #o #G #L #T #A #H
-@(gcr_aaa … (csx_gcp h o) (csx_gcr h o) … H)
-qed.
-
-(* Advanced eliminators *****************************************************)
-
-fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term.
-                      (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                            (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1
-                      ) →
-                      ∀T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ T ⁝ A → R T.
-#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
-qed-.
-
-lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term.
-                   (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                         (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1
-                   ) →
-                   ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
-/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-.
-
-fact aaa_ind_csx_alt_aux: ∀h,o,G,L,A. ∀R:predicate term.
-                          (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                                (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1
-                          ) →
-                          ∀T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ T ⁝ A → R T.
-#h #o #G #L #A #R #IH #T #H @(csx_ind_alt … H) -T /4 width=5 by cpxs_aaa_conf/
-qed-.
-
-lemma aaa_ind_csx_alt: ∀h,o,G,L,A. ∀R:predicate term.
-                       (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                             (∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 → (T1 = T2 → ⊥) → R T2) → R T1
-                       ) →
-                       ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
-/5 width=9 by aaa_ind_csx_alt_aux, aaa_csx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma
new file mode 100644
index 000000000..51596c44e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma
@@ -0,0 +1,100 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/predtysnstrong_5.ma".
+include "basic_2/static/lfdeq.ma".
+include "basic_2/rt_transition/lfpx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+
+definition lfsx: ∀h. sd h → relation3 term genv lenv ≝
+                 λh,o,T,G. SN … (lfpx h G T) (lfdeq h o T).
+
+interpretation
+   "strong normalization for uncounted context-sensitive parallel rt-transition on referred entries (local environment)"
+   'PRedTySNStrong h o T G L = (lfsx h o T G L).
+
+(* Basic eliminators ********************************************************)
+
+(* Basic_2A1: was: lsx_ind *)
+lemma lfsx_ind: ∀h,o,G,T. ∀R:predicate lenv.
+                (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+                      (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → R L2) →
+                      R L1
+                ) →
+                ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
+#h #o #G #T #R #H0 #L1 #H elim H -L1
+/5 width=1 by lfdeq_sym, SN_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: was: lsx_intro *)
+lemma lfsx_intro: ∀h,o,G,L1,T.
+                  (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
+                  G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
+/5 width=1 by lfdeq_sym, SN_intro/ qed.
+(*
+lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄.
+#h #o #G #L1 #s @lfsx_intro
+#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H *
+[ #H1 #H2 destruct //
+| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct 
+  @lfdeq_sort 
+qed.
+
+lemma lfsx_gref: ∀h,o,G,L,l,p. G ⊢ ⬈*[h, o, §p, l] L.
+#h #o #G #L1 #l #p @lfsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=4 by lfpx_fwd_length, lfdeq_gref/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lfsx_fwd_bind_sn: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L →
+                       G ⊢ ⬈*[h, o, V, l] L.
+#h #o #a #I #G #L #V #T #l #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=4 by lfdeq_fwd_bind_sn/
+qed-.
+
+lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+                       G ⊢ ⬈*[h, o, V, l] L.
+#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/
+qed-.
+
+lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+                       G ⊢ ⬈*[h, o, T, l] L.
+#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/
+qed-.
+
+lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L →
+                       G ⊢ ⬈*[h, o, V, l] L.
+#h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+                    G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L.
+/3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-.
+
+(* Basic_2A1: removed theorems 5:
+              lsx_atom lsx_sort lsx_gref lsx_ge_up lsx_ge
+*)
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqus.ma
new file mode 100644
index 000000000..789453aa9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqus.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/lfdeq_fqus.ma".
+include "basic_2/rt_computation/lfsx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: was: lsx_atom *)
+lemma lfsx_atom: ∀h,o,G,T. G ⊢ ⬈*[h, o, T] 𝐒⦃⋆⦄.
+#h #o #G #T @lfsx_intro
+#Y #H #HI lapply (lfpx_inv_atom_sn … H) -H
+#H destruct elim HI -HI //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx.ma
deleted file mode 100644
index 7bb8aec4a..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx.ma
+++ /dev/null
@@ -1,109 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/sn_6.ma".
-include "basic_2/multiple/lleq.ma".
-include "basic_2/reduction/lpx.ma".
-
-(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
-
-definition lsx: ∀h. sd h → relation4 ynat term genv lenv ≝
-                λh,o,l,T,G. SN … (lpx h o G) (lleq l T).
-
-interpretation
-   "extended strong normalization (local environment)"
-   'SN h o l T G L = (lsx h o T l G L).
-
-(* Basic eliminators ********************************************************)
-
-lemma lsx_ind: ∀h,o,G,T,l. ∀R:predicate lenv.
-               (∀L1. G ⊢ ⬊*[h, o, T, l] L1 →
-                     (∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → R L2) →
-                     R L1
-               ) →
-               ∀L. G ⊢ ⬊*[h, o, T, l] L → R L.
-#h #o #G #T #l #R #H0 #L1 #H elim H -L1
-/5 width=1 by lleq_sym, SN_intro/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsx_intro: ∀h,o,G,L1,T,l.
-                 (∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → G ⊢ ⬊*[h, o, T, l] L2) →
-                 G ⊢ ⬊*[h, o, T, l] L1.
-/5 width=1 by lleq_sym, SN_intro/ qed.
-
-lemma lsx_atom: ∀h,o,G,T,l. G ⊢ ⬊*[h, o, T, l] ⋆.
-#h #o #G #T #l @lsx_intro
-#X #H #HT lapply (lpx_inv_atom1 … H) -H
-#H destruct elim HT -HT //
-qed.
-
-lemma lsx_sort: ∀h,o,G,L,l,s. G ⊢ ⬊*[h, o, ⋆s, l] L.
-#h #o #G #L1 #l #s @lsx_intro
-#L2 #HL12 #H elim H -H
-/3 width=4 by lpx_fwd_length, lleq_sort/
-qed.
-
-lemma lsx_gref: ∀h,o,G,L,l,p. G ⊢ ⬊*[h, o, §p, l] L.
-#h #o #G #L1 #l #p @lsx_intro
-#L2 #HL12 #H elim H -H
-/3 width=4 by lpx_fwd_length, lleq_gref/
-qed.
-
-lemma lsx_ge_up: ∀h,o,G,L,T,U,lt,l,k. lt ≤ yinj l + yinj k →
-                 ⬆[l, k] T ≡ U → G ⊢ ⬊*[h, o, U, lt] L → G ⊢ ⬊*[h, o, U, l] L.
-#h #o #G #L #T #U #lt #l #k #Hltlm #HTU #H @(lsx_ind … H) -L
-/5 width=7 by lsx_intro, lleq_ge_up/
-qed-.
-
-lemma lsx_ge: ∀h,o,G,L,T,l1,l2. l1 ≤ l2 →
-              G ⊢ ⬊*[h, o, T, l1] L → G ⊢ ⬊*[h, o, T, l2] L.
-#h #o #G #L #T #l1 #l2 #Hl12 #H @(lsx_ind … H) -L
-/5 width=7 by lsx_intro, lleq_ge/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lsx_fwd_bind_sn: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓑ{a,I}V.T, l] L →
-                       G ⊢ ⬊*[h, o, V, l] L.
-#h #o #a #I #G #L #V #T #l #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 @lsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=4 by lleq_fwd_bind_sn/
-qed-.
-
-lemma lsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L →
-                       G ⊢ ⬊*[h, o, V, l] L.
-#h #o #I #G #L #V #T #l #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 @lsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_sn/
-qed-.
-
-lemma lsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L →
-                       G ⊢ ⬊*[h, o, T, l] L.
-#h #o #I #G #L #V #T #l #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 @lsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_dx/
-qed-.
-
-lemma lsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ②{I}V.T, l] L →
-                       G ⊢ ⬊*[h, o, V, l] L.
-#h #o * /2 width=4 by lsx_fwd_bind_sn, lsx_fwd_flat_sn/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L →
-                    G ⊢ ⬊*[h, o, V, l] L ∧ G ⊢ ⬊*[h, o, T, l] L.
-/3 width=3 by lsx_fwd_flat_sn, lsx_fwd_flat_dx, conj/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
index 2ed89fa2f..4269b54d2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
@@ -1,4 +1,5 @@
-cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
+cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
 lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma
 csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
 csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma 
+lfsx.ma lfsx_fqup.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma
index ad9f1e03f..0fc26a744 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma
@@ -54,10 +54,10 @@ lemma lfpx_pair_repl_dx: ∀h,I,G,L1,L2,T,V,V1.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma lfpx_inv_atom_sn: ∀h,I,G,Y2. ⦃G, ⋆⦄ ⊢ ⬈[h, ⓪{I}] Y2 → Y2 = ⋆.
+lemma lfpx_inv_atom_sn: ∀h,G,Y2,T. ⦃G, ⋆⦄ ⊢ ⬈[h, T] Y2 → Y2 = ⋆.
 /2 width=3 by lfxs_inv_atom_sn/ qed-.
 
-lemma lfpx_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ⬈[h, ⓪{I}] ⋆ → Y1 = ⋆.
+lemma lfpx_inv_atom_dx: ∀h,G,Y1,T. ⦃G, Y1⦄ ⊢ ⬈[h, T] ⋆ → Y1 = ⋆.
 /2 width=3 by lfxs_inv_atom_dx/ qed-.
 
 lemma lfpx_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] Y2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
index e49ccbfbe..aa6484ace 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
@@ -105,10 +105,10 @@ lemma lfdeq_pair_repl_dx: ∀h,o,I,L1,L2.∀T:term.∀V,V1.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma lfdeq_inv_atom_sn: ∀h,o,I,Y2. ⋆ ≡[h, o, ⓪{I}] Y2 → Y2 = ⋆.
+lemma lfdeq_inv_atom_sn: ∀h,o,Y2. ∀T:term. ⋆ ≡[h, o, T] Y2 → Y2 = ⋆.
 /2 width=3 by lfxs_inv_atom_sn/ qed-.
 
-lemma lfdeq_inv_atom_dx: ∀h,o,I,Y1. Y1 ≡[h, o, ⓪{I}] ⋆ → Y1 = ⋆.
+lemma lfdeq_inv_atom_dx: ∀h,o,Y1. ∀T:term. Y1 ≡[h, o, T] ⋆ → Y1 = ⋆.
 /2 width=3 by lfxs_inv_atom_dx/ qed-.
 
 lemma lfdeq_inv_zero: ∀h,o,Y1,Y2. Y1 ≡[h, o, #0] Y2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index 9f0a1a486..f754e46de 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -91,11 +91,11 @@ qed-.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆.
-#R #I #Y2 * /2 width=4 by lexs_inv_atom1/
+lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⦻*[R, T] Y2 → Y2 = ⋆.
+#R #Y2 #T * /2 width=4 by lexs_inv_atom1/
 qed-.
 
-lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆.
+lemma lfxs_inv_atom_dx: ∀R,Y1,T. Y1 ⦻*[R, T] ⋆ → Y1 = ⋆.
 #R #I #Y1 * /2 width=4 by lexs_inv_atom2/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index c1b25de72..5019e8956 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -116,7 +116,7 @@ table {
              [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
              [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
              [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ]
-             [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] 
+             [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] 
           }
         ]
      }