From bc40346f09bcccb9a09560963ccb7157ebfad7ad Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 13 Nov 2017 17:09:16 +0000
Subject: [PATCH] - lsubsx (replacement of lcosx) completed - minor updates

---
 .../relations/{clear_3.ml => lsubeqx_6.ma}    |   4 +-
 .../basic_2/rt_computation/lcosx.ma           |  77 ---------
 .../basic_2/rt_computation/lcosx_cpx.ma       |  67 --------
 .../basic_2/rt_computation/lfpxs_etc.ma       |  20 +++
 .../basic_2/rt_computation/lfsx_csx.ma        |   9 +-
 .../basic_2/rt_computation/lsubsx.ma          | 160 ++++++++++++++++++
 .../basic_2/rt_computation/lsubsx_lfsx.ma     |  64 +++++++
 .../lsubsx_lsubsx.ma}                         |  27 ++-
 .../basic_2/rt_computation/partial.txt        |   1 +
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |   4 +-
 10 files changed, 275 insertions(+), 158 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{clear_3.ml => lsubeqx_6.ma} (87%)
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx_cpx.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma
 rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/cosn_5.ma => rt_computation/lsubsx_lsubsx.ma} (54%)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/clear_3.ml b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lsubeqx_6.ma
similarity index 87%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/clear_3.ml
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lsubeqx_6.ma
index 09003e83a..7f9afe8ab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/clear_3.ml
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lsubeqx_6.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( L1 ⨵ [ break term 46 f ] break term 46 L2 )"
+notation "hvbox( G ⊢ break term 46 L1 ⊆ⓧ [ break term 46 h, break term 46 o, break term 46 f ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'Clear $f $L1 $L2 }.
+   for @{ 'LSubEqX $h $o $f $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx.ma
deleted file mode 100644
index 8f29e1aaf..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx.ma
+++ /dev/null
@@ -1,77 +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/cosn_5.ma".
-include "basic_2/computation/lsx.ma".
-
-(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
-
-inductive lcosx (h) (o) (G): relation2 ynat lenv ≝
-| lcosx_sort: ∀l. lcosx h o G l (⋆)
-| lcosx_skip: ∀I,L,T. lcosx h o G 0 L → lcosx h o G 0 (L.ⓑ{I}T)
-| lcosx_pair: ∀I,L,T,l. G ⊢ ⬊*[h, o, T, l] L →
-              lcosx h o G l L → lcosx h o G (⫯l) (L.ⓑ{I}T)
-.
-
-interpretation
-   "sn extended strong conormalization (local environment)"
-   'CoSN h o l G L = (lcosx h o G l L).
-
-(* Basic properties *********************************************************)
-
-lemma lcosx_O: ∀h,o,G,L. G ⊢ ~⬊*[h, o, 0] L.
-#h #o #G #L elim L /2 width=1 by lcosx_skip/
-qed.
-
-lemma lcosx_drop_trans_lt: ∀h,o,G,L,l. G ⊢ ~⬊*[h, o, l] L →
-                            ∀I,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → i < l →
-                            G ⊢ ~⬊*[h, o, ⫰(l-i)] K ∧ G ⊢ ⬊*[h, o, V, ⫰(l-i)] K.
-#h #o #G #L #l #H elim H -L -l
-[ #l #J #K #V #i #H elim (drop_inv_atom1 … H) -H #H destruct
-| #I #L #T #_ #_ #J #K #V #i #_ #H elim (ylt_yle_false … H) -H //
-| #I #L #T #l #HT #HL #IHL #J #K #V #i #H #Hil
-  elim (drop_inv_O1_pair1 … H) -H * #Hi #HLK destruct
-  [ >ypred_succ /2 width=1 by conj/
-  | lapply (ylt_pred … Hil ?) -Hil /2 width=1 by ylt_inj/ >ypred_succ #Hil
-    elim (IHL … HLK ?) -IHL -HLK <yminus_inj >yminus_SO2 //
-    <(ypred_succ l) in ⊢ (%→%→?); >yminus_pred /2 width=1 by ylt_inj, conj/
-  ]
-]
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lcosx_inv_succ_aux: ∀h,o,G,L,x. G ⊢ ~⬊*[h, o, x] L → ∀l. x = ⫯l →
-                         L = ⋆ ∨
-                         ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ~⬊*[h, o, l] K &
-                                  G ⊢ ⬊*[h, o, V, l] K.
-#h #o #G #L #l * -L -l /2 width=1 by or_introl/
-[ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H)
-| #I #L #T #l #HT #HL #x #H <(ysucc_inv_inj … H) -x
-  /3 width=6 by ex3_3_intro, or_intror/
-]
-qed-.
-
-lemma lcosx_inv_succ: ∀h,o,G,L,l. G ⊢ ~⬊*[h, o, ⫯l] L → L = ⋆ ∨
-                      ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ~⬊*[h, o, l] K &
-                               G ⊢ ⬊*[h, o, V, l] K.
-/2 width=3 by lcosx_inv_succ_aux/ qed-.
-
-lemma lcosx_inv_pair: ∀h,o,I,G,L,T,l. G ⊢ ~⬊*[h, o, ⫯l] L.ⓑ{I}T →
-                      G ⊢ ~⬊*[h, o, l] L ∧ G ⊢ ⬊*[h, o, T, l] L.
-#h #o #I #G #L #T #l #H elim (lcosx_inv_succ … H) -H
-[ #H destruct
-| * #Z #Y #X #H destruct /2 width=1 by conj/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx_cpx.ma
deleted file mode 100644
index 756b8a7a1..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lcosx_cpx.ma
+++ /dev/null
@@ -1,67 +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/lsx_drop.ma".
-include "basic_2/computation/lsx_lpx.ma".
-include "basic_2/computation/lsx_lpxs.ma".
-include "basic_2/computation/lcosx.ma".
-
-(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
-
-(* Properties on extended context-sensitive parallel reduction for term *****)
-
-lemma lsx_cpx_trans_lcosx: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 →
-                           ∀l. G ⊢ ~⬊*[h, o, l] L →
-                           G ⊢ ⬊*[h, o, T1, l] L → G ⊢ ⬊*[h, o, T2, l] L.
-#h #o #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
-[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #l #HL #H
-  elim (ylt_split i l) #Hli [ -H | -HL ]
-  [ <(ymax_pre_sn l (⫯i)) /2 width=1 by ylt_fwd_le_succ1/
-    elim (lcosx_drop_trans_lt … HL … HLK) // -HL -Hli
-    lapply (drop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
-  | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hli
-    lapply (drop_fwd_drop2 … HLK) -HLK
-    /4 width=10 by lsx_ge, lsx_lift_le/
-  ]
-| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
-  elim (lsx_inv_bind … H) -H #HV1 #HT1
-  @lsx_bind /2 width=2 by/ (**) (* explicit constructor *)
-  @(lsx_lreq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, lreq_succ/
-| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #l #HL #H
-  elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/
-| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #l #HL #H
-  elim (lsx_inv_bind … H) -H #HV #HU1
-  <(ypred_succ l) <yminus_SO2
-  /4 width=7 by lcosx_pair, lsx_inv_lift_ge, drop_drop/
-| #G #L #V #T1 #T2 #_ #IHT12 #l #HL #H
-  elim (lsx_inv_flat … H) -H /2 width=1 by/
-| #G #L #V1 #V2 #T #_ #IHV12 #l #HL #H
-  elim (lsx_inv_flat … H) -H /2 width=1 by/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #l #HL #H
-  elim (lsx_inv_flat … H) -H #HV1 #H
-  elim (lsx_inv_bind … H) -H #HW1 #HT1
-  @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *)
-  @(lsx_lreq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, lreq_succ/
-| #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #l #HL #H
-  elim (lsx_inv_flat … H) -H #HV1 #H
-  elim (lsx_inv_bind … H) -H #HW1 #HT1
-  @lsx_bind /2 width=1 by/ (**) (* explicit constructor *)
-  @lsx_flat [ <yplus_SO2 /3 width=7 by lsx_lift_ge, drop_drop/ ]
-  @(lsx_lreq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, lreq_succ/
-]
-qed-.
-
-lemma lsx_cpx_trans_O: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 →
-                       G ⊢ ⬊*[h, o, T1, 0] L → G ⊢ ⬊*[h, o, T2, 0] L.
-/2 width=3 by lsx_cpx_trans_lcosx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
new file mode 100644
index 000000000..0fda037b1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
@@ -0,0 +1,20 @@
+
+include "basic_2/static/lfxs_lfxs.ma".
+include "basic_2/rt_transition/lfpx_frees.ma".
+include "basic_2/rt_computation/lfpxs_fqup.ma".
+
+axiom cpx_frees_conf_lfpxs: ∀h,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
+                            ∀f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
+                            ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T1] L2 →
+                            ∀g1. L2 ⊢ 𝐅*⦃T1⦄ ≡ g1 →
+                            ∃∃g2. L2 ⊢ 𝐅*⦃T2⦄ ≡ g2 & g2 ⊆ g1 & g1 ⊆ f1.
+
+lemma lfpxs_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G).
+#h #G #L1 #T1 #T2 #HT12 #L2 #H
+lapply (cpx_frees_conf_lfpxs … HT12) -HT12 #HT12
+@(lfpxs_ind_sn … H) -L2 //
+#L #L2 #HL1 * #g1 #Hg1 #HL2 #IH
+elim (frees_total L1 T1) #f1 #Hf1
+elim (HT12 … Hf1 …  HL1 … Hg1) -T1 #g2 #Hg2 #Hg21 #_ -f1
+/4 width=7 by lfpxs_step_dx, sle_lexs_trans, ex2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma
index aa8e2c9da..862858c4a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma
@@ -12,11 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/rt_computation/lfpxs.ma".
 include "basic_2/rt_computation/csx_cpxs.ma".
 include "basic_2/rt_computation/csx_lsubr.ma".
-include "basic_2/rt_computation/lfsx_drops.ma".
-include "basic_2/rt_computation/lfsx_lfpxs.ma".
+include "basic_2/rt_computation/lsubsx_lfsx.ma".
 
 (* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
 
@@ -36,13 +34,12 @@ elim (tdeq_dec h o V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnY ]
 | @lfsx_lfpx_trans
   [2: @(IHV0 … HnV02 K0 … I) -IHV0 -HnV02
       [ /2 width=3 by lfpxs_cpx_trans/
-      |
+      | /2 width=3 by lfsx_cpx_trans/
       | 
       ]
   |1: skip
   |3: @lfpx_pair /2 width=3 by lfpx_cpx_conf/
-  ]  
-  /3 width=4 by lsx_cpx_trans_O, lsx_lpx_trans, lpxs_cpx_trans, lpxs_strap1/ (**) (* full auto too slow *)
+  ]
 ]
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma
new file mode 100644
index 000000000..01f64cfa6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx.ma
@@ -0,0 +1,160 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsubeqx_6.ma".
+include "basic_2/rt_computation/lfsx.ma".
+
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+
+(* Note: this should be an instance of a more general lexs *)
+(* Basic_2A1: uses: lcosx *)
+inductive lsubsx (h) (o) (G): rtmap → relation lenv ≝
+| lsubsx_atom: ∀f. lsubsx h o G f (⋆) (⋆)
+| lsubsx_push: ∀f,I,K1,K2. lsubsx h o G f K1 K2 →
+               lsubsx h o G (↑f) (K1.ⓘ{I}) (K2.ⓘ{I})
+| lsubsx_unit: ∀f,I,K1,K2. lsubsx h o G f K1 K2 →
+               lsubsx h o G (⫯f) (K1.ⓤ{I}) (K2.ⓧ)
+| lsubsx_pair: ∀f,I,K1,K2,V. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ →
+               lsubsx h o G f K1 K2 → lsubsx h o G (⫯f) (K1.ⓑ{I}V) (K2.ⓧ)
+.
+
+interpretation
+  "local environment refinement (clear)"
+  'LSubEqX h o f G L1 L2 = (lsubsx h o G f L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubsx_inv_atom_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
+                             L1 = ⋆ → L2 = ⋆.
+#h #o #g #G #L1 #L2 * -g -L1 -L2 //
+[ #f #I #K1 #K2 #_ #H destruct
+| #f #I #K1 #K2 #_ #H destruct
+| #f #I #K1 #K2 #V #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubsx_inv_atom_sn: ∀h,o,g,G,L2. G ⊢ ⋆ ⊆ⓧ[h, o, g] L2 → L2 = ⋆.
+/2 width=7 by lsubsx_inv_atom_sn_aux/ qed-.
+
+fact lsubsx_inv_push_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
+                             ∀f,I,K1. g = ↑f → L1 = K1.ⓘ{I} →
+                             ∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓘ{I}.
+#h #o #g #G #L1 #L2 * -g -L1 -L2
+[ #f #g #J #L1 #_ #H destruct
+| #f #I #K1 #K2 #HK12 #g #J #L1 #H1 #H2 destruct
+  <(injective_push … H1) -g /2 width=3 by ex2_intro/
+| #f #I #K1 #K2 #_ #g #J #L1 #H
+  elim (discr_next_push … H)
+| #f #I #K1 #K2 #V #_ #_ #g #J #L1 #H
+  elim (discr_next_push … H)
+]
+qed-.
+
+lemma lsubsx_inv_push_sn: ∀h,o,f,I,G,K1,L2. G ⊢ K1.ⓘ{I} ⊆ⓧ[h, o, ↑f] L2 →
+                          ∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓘ{I}.
+/2 width=5 by lsubsx_inv_push_sn_aux/ qed-.
+
+fact lsubsx_inv_unit_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
+                             ∀f,I,K1. g = ⫯f → L1 = K1.ⓤ{I} →
+                             ∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
+#h #o #g #G #L1 #L2 * -g -L1 -L2
+[ #f #g #J #L1 #_ #H destruct
+| #f #I #K1 #K2 #_ #g #J #L1 #H
+  elim (discr_push_next … H)
+| #f #I #K1 #K2 #HK12 #g #J #L1 #H1 #H2 destruct
+  <(injective_next … H1) -g /2 width=3 by ex2_intro/
+| #f #I #K1 #K2 #V #_ #_ #g #J #L1 #_ #H destruct
+]
+qed-.
+
+lemma lsubsx_inv_unit_sn: ∀h,o,f,I,G,K1,L2. G ⊢ K1.ⓤ{I} ⊆ⓧ[h, o, ⫯f] L2 →
+                          ∃∃K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
+/2 width=6 by lsubsx_inv_unit_sn_aux/ qed-.
+
+fact lsubsx_inv_pair_sn_aux: ∀h,o,g,G,L1,L2. G ⊢ L1 ⊆ⓧ[h, o, g] L2 →
+                             ∀f,I,K1,V. g = ⫯f → L1 = K1.ⓑ{I}V →
+                             ∃∃K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ &
+                                   G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
+#h #o #g #G #L1 #L2 * -g -L1 -L2
+[ #f #g #J #L1 #W #_ #H destruct
+| #f #I #K1 #K2 #_ #g #J #L1 #W #H
+  elim (discr_push_next … H)
+| #f #I #K1 #K2 #_ #g #J #L1 #W #_ #H destruct
+| #f #I #K1 #K2 #V #HV #HK12 #g #J #L1 #W #H1 #H2 destruct
+  <(injective_next … H1) -g /2 width=4 by ex3_intro/
+]
+qed-.
+
+(* Basic_2A1: uses: lcosx_inv_pair *)
+lemma lsubsx_inv_pair_sn: ∀h,o,f,I,G,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊆ⓧ[h, o, ⫯f] L2 →
+                          ∃∃K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ &
+                                G ⊢ K1 ⊆ⓧ[h, o, f] K2 & L2 = K2.ⓧ.
+/2 width=6 by lsubsx_inv_pair_sn_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lsubsx_inv_pair_sn_gen: ∀h,o,g,I,G,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊆ⓧ[h, o, g] L2 →
+                              ∨∨ ∃∃f,K2. G ⊢ K1 ⊆ⓧ[h, o, f] K2 & g = ↑f & L2 = K2.ⓑ{I}V
+                               | ∃∃f,K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ &
+                                         G ⊢ K1 ⊆ⓧ[h, o, f] K2 & g = ⫯f & L2 = K2.ⓧ.
+#h #o #g #I #G #K1 #L2 #V #H
+elim (pn_split g) * #f #Hf destruct
+[ elim (lsubsx_inv_push_sn … H) -H /3 width=5 by ex3_2_intro, or_introl/
+| elim (lsubsx_inv_pair_sn … H) -H /3 width=6 by ex4_2_intro, or_intror/
+]
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lsubsx_fwd_bind_sn: ∀h,o,g,I1,G,K1,L2. G ⊢ K1.ⓘ{I1} ⊆ⓧ[h, o, g] L2 →
+                          ∃∃I2,K2. G ⊢ K1 ⊆ⓧ[h, o, ⫱g] K2 & L2 = K2.ⓘ{I2}.
+#h #o #g #I1 #G #K1 #L2
+elim (pn_split g) * #f #Hf destruct
+[ #H elim (lsubsx_inv_push_sn … H) -H
+| cases I1 -I1 #I1
+  [ #H elim (lsubsx_inv_unit_sn … H) -H
+  | #V #H elim (lsubsx_inv_pair_sn … H) -H
+  ]
+]
+/2 width=4 by ex2_2_intro/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsubsx_eq_repl_back: ∀h,o,G,L1,L2. eq_repl_back … (λf. G ⊢ L1 ⊆ⓧ[h, o, f] L2).
+#h #o #G #L1 #L2 #f1 #H elim H -L1 -L2 -f1 //
+[ #f #I #L1 #L2 #_ #IH #x #H
+  elim (eq_inv_px … H) -H /3 width=3 by lsubsx_push/
+| #f #I #L1 #L2 #_ #IH #x #H
+  elim (eq_inv_nx … H) -H /3 width=3 by lsubsx_unit/
+| #f #I #L1 #L2 #V #HV #_ #IH #x #H
+  elim (eq_inv_nx … H) -H /3 width=3 by lsubsx_pair/
+]
+qed-.
+
+lemma lsubsx_eq_repl_fwd: ∀h,o,G,L1,L2. eq_repl_fwd … (λf. G ⊢ L1 ⊆ⓧ[h, o, f] L2).
+#h #o #G #L1 #L2 @eq_repl_sym /2 width=3 by lsubsx_eq_repl_back/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lcosx_O *)
+lemma lsubsx_refl: ∀h,o,f,G. 𝐈⦃f⦄ → reflexive … (lsubsx h o G f).
+#h #o #f #G #Hf #L elim L -L
+/3 width=3 by lsubsx_eq_repl_back, lsubsx_push, eq_push_inv_isid/
+qed.
+
+(* Basic_2A1: removed theorems 2:
+              lcosx_drop_trans_lt lcosx_inv_succ
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma
new file mode 100644
index 000000000..4ef9cf962
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lfsx.ma
@@ -0,0 +1,64 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/rt_computation/lfsx_drops.ma".
+include "basic_2/rt_computation/lfsx_lfpxs.ma".
+include "basic_2/rt_computation/lsubsx.ma".
+
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+
+(* Properties with strong normalizing env's for uncounted rt-transition *****)
+
+(* Basic_2A1: uses: lsx_cpx_trans_lcosx *)
+lemma lfsx_cpx_trans_lsubsx: ∀h,o,G,L0,T1,T2. ⦃G, L0⦄ ⊢ T1 ⬈[h] T2 →
+                             ∀f,L. G ⊢ L0 ⊆ⓧ[h, o, f] L →
+                             G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
+#h #o #G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2 //
+[ #I0 #G #K0 #V1 #V2 #W2 #_ #IH #HVW2 #g #L #HK0 #HL
+  elim (lsubsx_inv_pair_sn_gen … HK0) -HK0 *
+  [ #f #K #HK0 #H1 #H2 destruct
+    /4 width=8 by lfsx_lifts, lfsx_fwd_pair, drops_refl, drops_drop/
+  | #f #K #HV1 #HK0 #H1 #H2 destruct
+    /4 width=8 by lfsx_lifts, drops_refl, drops_drop/
+  ]
+| #I0 #G #K0 #T #U #i #_ #IH #HTU #g #L #HK0 #HL
+  elim (lsubsx_fwd_bind_sn … HK0) -HK0 #I #K #HK0 #H destruct
+  /6 width=8 by lfsx_inv_lifts, lfsx_lifts, drops_refl, drops_drop/
+| #p #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
+  elim (lfsx_inv_bind … HL) -HL
+  /4 width=2 by lsubsx_pair, lfsx_bind_void/
+| #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
+  elim (lfsx_inv_flat … HL) -HL /3 width=2 by lfsx_flat/
+| #G #L0 #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #f #L #HL0 #HL
+  elim (lfsx_inv_bind … HL) -HL #HV #HU1
+  /4 width=8 by lsubsx_pair, lfsx_inv_lifts, drops_refl, drops_drop/
+| #G #L0 #V #T1 #T2 #_ #IHT12 #f #L #HL0 #HL
+  elim (lfsx_inv_flat … HL) -HL /2 width=2 by/
+| #G #L0 #V1 #V2 #T #_ #IHV12 #f #L #HL0 #HL
+  elim (lfsx_inv_flat … HL) -HL /2 width=2 by/
+| #p #G #L0 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #f #L #HL0 #HL
+  elim (lfsx_inv_flat … HL) -HL #HV1 #HL
+  elim (lfsx_inv_bind … HL) -HL #HW1 #HT1
+  /4 width=2 by lsubsx_pair, lfsx_bind_void, lfsx_flat/
+| #p #G #L0 #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #HVU2 #f #L #HL0 #HL
+  elim (lfsx_inv_flat … HL) -HL #HV1 #HL
+  elim (lfsx_inv_bind … HL) -HL #HW1 #HT1
+  /6 width=8 by lsubsx_pair, lfsx_lifts, lfsx_bind_void, lfsx_flat, drops_refl, drops_drop/
+]
+qed-.
+
+(* Basic_2A1: uses: lsx_cpx_trans_O *)
+lemma lfsx_cpx_trans: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
+                      G ⊢ ⬈*[h, o, T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T2] 𝐒⦃L⦄.
+/3 width=6 by lfsx_cpx_trans_lsubsx, lsubsx_refl/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lsubsx.ma
similarity index 54%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma
rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lsubsx.ma
index e69a4ac02..cf0daeaf4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubsx_lsubsx.ma
@@ -12,8 +12,27 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+include "basic_2/rt_computation/lsubsx.ma".
 
-notation "hvbox( G ⊢ ~ ⬊ * [ break term 46 h , break term 46 o , break term 46 f ] break term 46 L )"
-   non associative with precedence 45
-   for @{ 'CoSN $h $o $f $G $L }.
+(* CLEAR OF STRONGLY NORMALIZING ENTRIES FOR UNCOUNTED RT-TRANSITION ********)
+
+(* Main properties **********************************************************)
+
+theorem lsubsx_fix: ∀h,o,f,G,L1,L. G ⊢ L1 ⊆ⓧ[h, o, f] L →
+                    ∀L2. G ⊢ L ⊆ⓧ[h, o, f] L2 → L = L2.
+#h #o #f #G #L1 #L #H elim H -f -L1 -L
+[ #f #L2 #H
+  >(lsubsx_inv_atom_sn … H) -L2 //
+| #f #I #K1 #K2 #_ #IH #L2 #H
+  elim (lsubsx_inv_push_sn … H) -H /3 width=1 by eq_f2/
+| #f #I #K1 #K2 #_ #IH #L2 #H
+  elim (lsubsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/
+| #f #I #K1 #K2 #V #_ #_ #IH #L2 #H
+  elim (lsubsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/
+]
+qed-.
+
+theorem lsubsx_trans: ∀h,o,f,G. Transitive … (lsubsx h o G f).
+#h #o #f #G #L1 #L #H1 #L2 #H2
+<(lsubsx_fix … H1 … H2) -L2 //
+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 079fa87e0..acdc797e9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
@@ -3,3 +3,4 @@ lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.m
 csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma
 csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma 
 lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lfpxs.ma lfsx_lfsx.ma
+lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma
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 8ff7a521f..5719d23da 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
@@ -87,7 +87,6 @@ table {
           }
         ]
         [ { "strongly normalizing rt-computation" * } {
-             [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ]
              [ "llsx_csx" * ]
              [ "csx_fpbs" * ]
           }
@@ -106,8 +105,9 @@ table {
              [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
           }
         ]
-*)        
+*)
         [ { "uncounted context-sensitive rt-computation" * } {
+             [ "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
              [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
              [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
              [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
-- 
2.39.2