From 2368e490e9b948097cee58ae7c9d4915d1c3746f Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 8 Jun 2013 20:21:50 +0000
Subject: [PATCH] more results on extended reduction

---
 .../basic_2/computation/cprs_aaa.ma           |   2 +-
 .../basic_2/computation/lprs_aaa.ma           |   2 +-
 .../contribs/lambdadelta/basic_2/notation.ma  |  28 +-
 .../lambdadelta/basic_2/reduction/cpr.ma      |   2 +-
 .../lambdadelta/basic_2/reduction/cpx.ma      | 276 ++++++++++++++++--
 .../basic_2/reduction/cpx_ldrop.ma            |  64 ----
 .../lambdadelta/basic_2/reduction/cpx_lift.ma | 130 +++++++++
 .../lambdadelta/basic_2/reduction/lpx.ma      |  73 +++++
 .../reduction/{lpr_aaa.ma => lpx_aaa.ma}      |  40 +--
 .../basic_2/reduction/lpx_ldrop.ma            |  30 ++
 .../lambdadelta/basic_2/relocation/fsup.ma    |   5 +-
 .../lambdadelta/basic_2/relocation/fsupq.ma   |  50 +++-
 .../contribs/lambdadelta/basic_2/static/sh.ma |   3 +
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |   9 +-
 14 files changed, 592 insertions(+), 122 deletions(-)
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma
 rename matita/matita/contribs/lambdadelta/basic_2/reduction/{lpr_aaa.ma => lpx_aaa.ma} (70%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma
index 389e241ee..faeb6a633 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_aaa.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpr_aaa.ma".
+include "basic_2/reduction/lpx_aaa.ma".
 include "basic_2/computation/cprs.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_aaa.ma
index c5b653092..eb94c05ee 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_aaa.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpr_aaa.ma".
+include "basic_2/reduction/lpx_aaa.ma".
 include "basic_2/computation/lprs.ma".
 
 (* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index b956f9049..c8c98ecfc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -254,17 +254,17 @@ notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )"
    non associative with precedence 45
    for @{ 'PRed $L $T1 $T2 }.
 
-notation "hvbox( L1 ⊢ ➡ break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'PRedSn $L1 $L2 }.
-
 notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 g ] break term 46 T2 )"
    non associative with precedence 45
    for @{ 'PRed $h $g $L $T1 $T2 }.
 
-notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ ➡ break [ term 46 g ] break term 46 T2 )"
+notation "hvbox( L1 ⊢ ➡ break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'PRedSn $L1 $L2 }.
+
+notation "hvbox( ⦃ term 46 h, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 g ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'PRedAlt $h $g $L $T1 $T2 }.
+   for @{ 'PRedSn $h $g $L1 $L2 }.
 
 (* Computation **************************************************************)
 
@@ -284,10 +284,6 @@ notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )"
    non associative with precedence 45
    for @{ 'PEval $L $T1 $T2 }.
 
-notation "hvbox( ⬊ * term 46 T )"
-   non associative with precedence 45
-   for @{ 'SN $T }.
-
 notation "hvbox( L ⊢ ⬊ * break term 46 T )"
    non associative with precedence 45
    for @{ 'SN $L $T }.
@@ -296,6 +292,18 @@ notation "hvbox( L ⊢ ⬊ ⬊ * break term 46 T )"
    non associative with precedence 45
    for @{ 'SNAlt $L $T }.
 
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 g ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRedStar $h $g $L $T1 $T2 }.
+
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 g ] break term 46 T )"
+   non associative with precedence 45
+   for @{ 'SN $h $g $L $T }.
+
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ ⬊ * break [ term 46 g ] break term 46 T )"
+   non associative with precedence 45
+   for @{ 'SNAlt $h $g $L $T }.
+
 notation "hvbox( ⦃ term 46 L, break term 46 T ⦄ ϵ break [ term 46 R ] break 〚term 46  A 〛 )"
    non associative with precedence 45
    for @{ 'InEInt $R $L $T $A }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
index 329958fb6..10430b3a1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
@@ -75,7 +75,7 @@ lemma cpr_refl: ∀T,L. L ⊢ T ➡ T.
 
 (* Basic_1: was: pr2_head_1 *)
 lemma cpr_pair_sn: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 →
-                   ∀T. L⊢ ②{I}V1.T ➡ ②{I}V2.T.
+                   ∀T. L ⊢ ②{I}V1.T ➡ ②{I}V2.T.
 * /2 width=1/ qed.
 
 lemma cpr_delift: ∀L,K,V,T1,d. ⇩[0, d] L ≡ (K. ⓓV) →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index 0c6d10fa1..935d5c7b0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
@@ -18,12 +18,26 @@ include "basic_2/reduction/cpr.ma".
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
 
 inductive cpx (h) (g): lenv → relation term ≝
-| cpx_cpr : ∀I,L,U2. L ⊢ ⓪{I} ➡ U2 → cpx h g L (⓪{I}) U2
-| cpx_ssta: ∀I,L,U2,l. ⦃h, L⦄ ⊢ ⓪{I} •[g] ⦃l+1, U2⦄ → cpx h g L (⓪{I}) U2
-| cpx_bind: ∀a,I,L,V1,V2,T1,T2,U2. cpx h g L V1 V2 → cpx h g (L.ⓑ{I}V1) T1 T2 →
-            L ⊢ ⓑ{a,I}V2.T2 ➡ U2 → cpx h g L (ⓑ{a,I}V1.T1) U2
-| cpx_flat: ∀I,L,V1,V2,T1,T2,U2. cpx h g L V1 V2 → cpx h g L T1 T2 →
-            L ⊢ ⓕ{I}V2.T2 ➡ U2 → cpx h g L (ⓕ{I}V1.T1) U2
+| cpx_atom : ∀I,L. cpx h g L (⓪{I}) (⓪{I})
+| cpx_sort : ∀L,k,l. deg h g k (l+1) → cpx h g L (⋆k) (⋆(next h k))
+| cpx_delta: ∀I,L,K,V,V2,W2,i.
+             ⇩[0, i] L ≡ K.ⓑ{I}V → cpx h g K V V2 →
+             ⇧[0, i + 1] V2 ≡ W2 → cpx h g L (#i) W2
+| cpx_bind : ∀a,I,L,V1,V2,T1,T2.
+             cpx h g L V1 V2 → cpx h g (L. ⓑ{I} V1) T1 T2 →
+             cpx h g L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
+| cpx_flat : ∀I,L,V1,V2,T1,T2.
+             cpx h g L V1 V2 → cpx h g L T1 T2 →
+             cpx h g L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
+| cpx_zeta : ∀L,V,T1,T,T2. cpx h g (L.ⓓV) T1 T →
+             ⇧[0, 1] T2 ≡ T → cpx h g L (+ⓓV. T1) T2
+| cpx_tau  : ∀L,V,T1,T2. cpx h g L T1 T2 → cpx h g L (ⓝV. T1) T2
+| cpx_beta : ∀a,L,V1,V2,W,T1,T2.
+             cpx h g L V1 V2 → cpx h g (L.ⓛW) T1 T2 →
+             cpx h g L (ⓐV1. ⓛ{a}W. T1) (ⓓ{a}V2. T2)
+| cpx_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2.
+             cpx h g L V1 V → ⇧[0, 1] V ≡ V2 → cpx h g L W1 W2 → cpx h g (L.ⓓW1) T1 T2 →
+             cpx h g L (ⓐV1. ⓓ{a}W1. T1) (ⓓ{a}W2. ⓐV2. T2)
 .
 
 interpretation
@@ -34,20 +48,246 @@ interpretation
 
 (* Note: this is "∀h,g,L. reflexive … (cpx h g L)" *)
 lemma cpx_refl: ∀h,g,T,L. ⦃h, L⦄ ⊢ T ➡[g] T.
-#h #g #T elim T -T /2 width=1/ * /2 width=5/
+#h #g #T elim T -T // * /2 width=1/
 qed.
 
-lemma cpr_cpx: ∀h,g,T1,L,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
-#h #g #T1 elim T1 -T1 /2 width=1/ * /2 width=5/
+lemma cpr_cpx: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+#h #g #L #T1 #T2 #H elim H -L -T1 -T2 // /2 width=1/ /2 width=3/ /2 width=7/
 qed.
 
-lemma ssta_cpx: ∀h,g,T1,L,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
-#h #g #T1 elim T1 -T1 /2 width=2/ * [|*]
-[ #a #I #V1 #T1 #_ #IHT1 #L #X #l #H
-  elim (ssta_inv_bind1 … H) -H #T2 #HT12 #H destruct /3 width=5/
-| #V1 #T1 #_ #IHT1 #L #X #l #H
-  elim (ssta_inv_appl1 … H) -H #T2 #HT12 #H destruct /3 width=5/
-| #V1 #T1 #_ #IHT1 #L #X #l #H
-  lapply (ssta_inv_cast1 … H) -H /3 width=5/
-]
+fact ssta_cpx_aux: ∀h,g,L,T1,T2,l0. ⦃h, L⦄ ⊢ T1 •[g] ⦃l0, T2⦄ →
+                   ∀l. l0 = l+1 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+#h #g #L #T1 #T2 #l0 #H elim H -L -T1 -T2 -l0 /2 width=2/ /2 width=7/ /3 width=2/ /3 width=7/
+qed-.
+
+lemma ssta_cpx: ∀h,g,L,T1,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+/2 width=4 by ssta_cpx_aux/ qed.
+
+lemma cpx_pair_sn: ∀h,g,I,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 →
+                   ∀T. ⦃h, L⦄ ⊢ ②{I}V1.T ➡[g] ②{I}V2.T.
+#h #g * /2 width=1/ qed.
+
+lemma cpx_delift: ∀h,g,L,K,V,T1,d. ⇩[0, d] L ≡ (K. ⓓV) →
+                  ∃∃T2,T.  ⦃h, L⦄ ⊢ T1 ➡[g] T2 & ⇧[d, 1] T ≡ T2.
+#h #g #L #K #V #T1 #d #HLK
+elim (cpr_delift … HLK) -HLK /3 width=4/
+qed-.
+
+lemma cpx_append: ∀h,g. l_appendable_sn … (cpx h g).
+#h #g #K #T1 #T2 #H elim H -K -T1 -T2 // /2 width=1/ /2 width=3/
+#I #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
+lapply (ldrop_fwd_ldrop2_length … HK0) #H
+@(cpx_delta … I … (L@@K0) V1 … HVW2) //
+@(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *)
 qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact cpx_inv_atom1_aux: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ∀J. T1 = ⓪{J} →
+                        ∨∨ T2 = ⓪{J}
+                         | ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k) & J = Sort k
+                         | ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊢ V ➡[g] V2 &
+                                         ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+#h #g #L #T1 #T2 * -L -T1 -T2
+[ #I #L #J #H destruct /2 width=1/
+| #L #k #l #Hkl #J #H destruct /3 width=5/
+| #I #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=9/
+| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #L #V #T1 #T #T2 #_ #_ #J #H destruct
+| #L #V #T1 #T2 #_ #J #H destruct
+| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #J #H destruct
+| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #J #H destruct
+]
+qed-.
+
+lemma cpx_inv_atom1: ∀h,g,J,L,T2. ⦃h, L⦄ ⊢ ⓪{J} ➡[g] T2 →
+                     ∨∨ T2 = ⓪{J}
+                      | ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k) & J = Sort k
+                      | ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊢ V ➡[g] V2 &
+                                      ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+/2 width=3 by cpx_inv_atom1_aux/ qed-.
+
+lemma cpx_inv_sort1: ∀h,g,L,T2,k. ⦃h, L⦄ ⊢ ⋆k ➡[g] T2 → T2 = ⋆k ∨
+                     ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k).
+#h #g #L #T2 #k #H
+elim (cpx_inv_atom1 … H) -H /2 width=1/ *
+[ #k0 #l #Hkl #H1 #H2 destruct /3 width=4/
+| #I #K #V #V2 #i #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma cpx_inv_lref1: ∀h,g,L,T2,i. ⦃h, L⦄ ⊢ #i ➡[g] T2 →
+                     T2 = #i ∨
+                     ∃∃I,K,V,V2. ⇩[O, i] L ≡ K. ⓑ{I}V & ⦃h, K⦄ ⊢ V ➡[g] V2 &
+                                 ⇧[O, i + 1] V2 ≡ T2.
+#h #g #L #T2 #i #H
+elim (cpx_inv_atom1 … H) -H /2 width=1/ *
+[ #k #l #_ #_ #H destruct
+| #I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7/
+]
+qed-.
+
+lemma cpx_inv_gref1: ∀h,g,L,T2,p.  ⦃h, L⦄ ⊢ §p ➡[g] T2 → T2 = §p.
+#h #g #L #T2 #p #H
+elim (cpx_inv_atom1 … H) -H // *
+[ #k #l #_ #_ #H destruct
+| #I #K #V #V2 #i #_ #_ #_ #H destruct
+]
+qed-.
+
+fact cpx_inv_bind1_aux: ∀h,g,L,U1,U2. ⦃h, L⦄ ⊢ U1 ➡[g] U2 →
+                        ∀a,J,V1,T1. U1 = ⓑ{a,J} V1. T1 → (
+                        ∃∃V2,T2.  ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{J}V1⦄ ⊢ T1 ➡[g] T2 &
+                                  U2 = ⓑ{a,J} V2. T2
+                        ) ∨
+                        ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T &
+                             a = true & J = Abbr.
+#h #g #L #U1 #U2 * -L -U1 -U2
+[ #I #L #b #J #W1 #U1 #H destruct
+| #L #k #l #_ #b #J #W1 #U1 #H destruct
+| #I #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W1 #U1 #H destruct
+| #a #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W1 #U1 #H destruct /3 width=5/
+| #I #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct
+| #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W1 #U1 #H destruct /3 width=3/
+| #L #V #T1 #T2 #_ #b #J #W1 #U1 #H destruct
+| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct
+| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #b #J #W1 #U1 #H destruct
+]
+qed-.
+
+lemma cpx_inv_bind1: ∀h,g,a,I,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡[g] U2 → (
+                     ∃∃V2,T2.  ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{I}V1⦄ ⊢ T1 ➡[g] T2 &
+                               U2 = ⓑ{a,I} V2. T2
+                     ) ∨
+                     ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T &
+                          a = true & I = Abbr.
+/2 width=3 by cpx_inv_bind1_aux/ qed-.
+
+lemma cpx_inv_abbr1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓓ{a}V1.T1 ➡[g] U2 → (
+                     ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓓ V1⦄ ⊢ T1 ➡[g] T2 &
+                              U2 = ⓓ{a} V2. T2
+                     ) ∨
+                     ∃∃T.  ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T & a = true.
+#h #g #a #L #V1 #T1 #U2 #H
+elim (cpx_inv_bind1 … H) -H * /3 width=3/ /3 width=5/
+qed-.
+
+lemma cpx_inv_abst1: ∀h,g,a,L,V1,T1,U2.  ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 ➡[g] U2 →
+                     ∃∃V2,T2.  ⦃h, L⦄ ⊢ V1 ➡[g] V2 &  ⦃h, L.ⓛ V1⦄ ⊢ T1 ➡[g] T2 &
+                               U2 = ⓛ{a} V2. T2.
+#h #g #a #L #V1 #T1 #U2 #H
+elim (cpx_inv_bind1 … H) -H *
+[ /3 width=5/
+| #T #_ #_ #_ #H destruct
+]
+qed-.
+
+fact cpx_inv_flat1_aux: ∀h,g,L,U,U2. ⦃h, L⦄ ⊢ U ➡[g] U2 →
+                        ∀J,V1,U1. U = ⓕ{J} V1. U1 →
+                        ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
+                                    U2 = ⓕ{J} V2. T2
+                         | (⦃h, L⦄ ⊢ U1 ➡[g] U2 ∧ J = Cast)
+                         | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 &
+                                           U1 = ⓛ{a}W. T1 &
+                                           U2 = ⓓ{a}V2. T2 & J = Appl
+                         | ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 &
+                                                 ⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 &
+                                                 U1 = ⓓ{a}W1. T1 &
+                                                 U2 = ⓓ{a}W2. ⓐV2. T2 & J = Appl.
+#h #g #L #U #U2 * -L -U -U2
+[ #I #L #J #W1 #U1 #H destruct
+| #L #k #l #_ #J #W1 #U1 #H destruct
+| #I #L #K #V #V2 #W2 #i #_ #_ #_ #J #W1 #U1 #H destruct
+| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #W1 #U1 #H destruct
+| #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /3 width=5/
+| #L #V #T1 #T #T2 #_ #_ #J #W1 #U1 #H destruct
+| #L #V #T1 #T2 #HT12 #J #W1 #U1 #H destruct /3 width=1/
+| #a #L #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /3 width=9/
+| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W1 #U1 #H destruct /3 width=13/
+]
+qed-.
+
+lemma cpx_inv_flat1: ∀h,g,I,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓕ{I}V1.U1 ➡[g] U2 →
+                     ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
+                                 U2 = ⓕ{I} V2. T2
+                      | (⦃h, L⦄ ⊢ U1 ➡[g] U2 ∧ I = Cast)
+                      | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 &
+                                        U1 = ⓛ{a}W. T1 &
+                                        U2 = ⓓ{a}V2. T2 & I = Appl
+                      | ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 &
+                                              ⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 &
+                                              U1 = ⓓ{a}W1. T1 &
+                                              U2 = ⓓ{a}W2. ⓐV2. T2 & I = Appl.
+/2 width=3 by cpx_inv_flat1_aux/ qed-.
+
+lemma cpx_inv_appl1: ∀h,g,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓐ V1.U1 ➡[g] U2 →
+                     ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
+                                 U2 = ⓐ V2. T2
+                      | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 &
+                                        U1 = ⓛ{a}W. T1 & U2 = ⓓ{a}V2. T2
+                      | ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 &
+                                              ⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 &
+                                              U1 = ⓓ{a}W1. T1 & U2 = ⓓ{a}W2. ⓐV2. T2.
+#h #g #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H *
+[ /3 width=5/
+| #_ #H destruct
+| /3 width=9/
+| /3 width=13/
+]
+qed-.
+
+(* Note: the main property of simple terms *)
+lemma cpx_inv_appl1_simple: ∀h,g,L,V1,T1,U. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡[g] U → 𝐒⦃T1⦄ →
+                            ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ T1 ➡[g] T2 &
+                                     U = ⓐV2. T2.
+#h #g #L #V1 #T1 #U #H #HT1
+elim (cpx_inv_appl1 … H) -H *
+[ /2 width=5/
+| #a #V2 #W #U1 #U2 #_ #_ #H #_ destruct
+  elim (simple_inv_bind … HT1)
+| #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
+  elim (simple_inv_bind … HT1)
+]
+qed-.
+
+lemma cpx_inv_cast1: ∀h,g,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓝ V1.U1 ➡[g] U2 → (
+                     ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
+                              U2 = ⓝ V2. T2
+                     ) ∨ ⦃h, L⦄ ⊢ U1 ➡[g] U2.
+#h #g #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H *
+[ /3 width=5/
+| /2 width=1/
+| #a #V2 #W #T1 #T2 #_ #_ #_ #_ #H destruct
+| #a #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpx_fwd_bind1_minus: ∀h,g,I,L,V1,T1,T. ⦃h, L⦄ ⊢ -ⓑ{I}V1.T1 ➡[g] T → ∀b.
+                           ∃∃V2,T2. ⦃h, L⦄ ⊢ ⓑ{b,I}V1.T1 ➡[g] ⓑ{b,I}V2.T2 &
+                                    T = -ⓑ{I}V2.T2.
+#h #g #I #L #V1 #T1 #T #H #b
+elim (cpx_inv_bind1 … H) -H *
+[ #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/
+| #T2 #_ #_ #H destruct 
+]
+qed-.
+
+lemma cpx_fwd_shift1: ∀h,g,L1,L,T1,T. ⦃h, L⦄ ⊢ L1 @@ T1 ➡[g] T →
+                      ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#h #g #L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #L #T1 #T #HT1
+  @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #L #T1 #X
+  >shift_append_assoc normalize #H
+  elim (cpx_inv_bind1 … H) -H *
+  [ #V0 #T0 #_ #HT10 #H destruct
+    elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
+    >append_length >HL12 -HL12
+    @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *)
+  | #T #_ #_ #H destruct
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma
deleted file mode 100644
index 20445e154..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_ldrop.ma
+++ /dev/null
@@ -1,64 +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/reduction/cpx.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
-
-include "basic_2/substitution/lpss_ldrop.ma".
-include "basic_2/substitution/fsups.ma".
-
-lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 →
-                       ∃∃U1. L1 ⊢ T1 ▶* U1 & ⦃L1, U1⦄ ⊃ ⦃L2, U2⦄.
-#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2: * ] [1,2,3,4,5: /3 width=5/ ]
-[ * #L1
-  [ #V2 #U2 #HVU2
-    elim (lift_total U2 0 1) #W2 #HUW2
-    @(ex2_intro … W2) /2 width=7/
-    @(fsup_ldrop … L1 … HUW2) /2 width=1/
-  | #W #U2 #H  
-    @(ex2_intro … (#0)) /2 width=7/
-  
-| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
-  elim (IHT12 … HTU2) -IHT12 -HTU2 #T #HT1 #HT2
-  elim (lift_total T d e) #U #HTU
-  lapply (cpss_lift … HT1 … HLK1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
-]
-qed-.
-
-
-
-(*
-include "basic_2/relocation/lift_lift.ma".
-include "basic_2/substitution/fsups.ma".
-*)
-(*
-lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
-                       ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
-                       ∃∃L,U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄.
-
-*)
-lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
-                       ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
-                       ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃ ⦃L2, U2⦄.
-#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
-[ * #L1 #V1 #U2 #l #H
-  elim (lift_total U2 0 1) #W2 #HUW2
-(*
-  [ @(ex2_intro … W2) [ @(cpx_ssta … l) @(ssta_ldef … H) //
-                      | @(fsups_ldrop … L1 … HUW2) /2 width=1/ 
-*)
-|
-| #a #I #L1 #V1 #T1 #U2 #l #HT1
-  @(ex2_intro … (ⓑ{a,I}V1.U2)) /2 width=1/  
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
new file mode 100644
index 000000000..427c0a28b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -0,0 +1,130 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/ldrop_ldrop.ma".
+include "basic_2/relocation/fsupq.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Relocation properties ****************************************************)
+
+lemma cpx_lift: ∀h,g. l_liftable (cpx h g).
+#h #g #K #T1 #T2 #H elim H -K -T1 -T2
+[ #I #K #L #d #e #_ #U1 #H1 #U2 #H2
+  >(lift_mono … H1 … H2) -H1 -H2 //
+| #K #k #l #Hkl #L #d #e #_ #U1 #H1 #U2 #H2
+  >(lift_inv_sort1 … H1) -U1
+  >(lift_inv_sort1 … H2) -U2 /2 width=2/
+| #I #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
+    elim (ldrop_trans_le … HLK … HKV) -K /2 width=2/ #X #HLK #H
+    elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #K #Y #HKV #HVY #H destruct /3 width=9/
+  | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 // /2 width=1/ >plus_plus_comm_23 #HVU2
+    lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=7/
+  ]
+| #a #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+  elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+  elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/
+| #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+  elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/
+| #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2
+  elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
+  elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/
+| #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2
+  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/
+| #a #K #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+  elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
+  elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
+  elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /4 width=5/
+| #a #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+  elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
+  elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
+  elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct
+  elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct
+  elim (lift_trans_ge … HV2 … HV3 ?) -V2 // /4 width=5/
+]
+qed.
+
+lemma cpx_inv_lift1: ∀h,g. l_deliftable_sn (cpx h g).
+#h #g #L #U1 #U2 #H elim H -L -U1 -U2
+[ * #L #i #K #d #e #_ #T1 #H
+  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
+  | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/
+  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/
+  ]
+| #L #k #l #Hkl #K #d #e #_ #T1 #H
+  lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3/
+| #I #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
+  elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+  [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
+    elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
+    elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m // -Hid /3 width=9/
+  | elim (le_inv_plus_l … Hid) #Hdie #Hei
+    lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
+    elim (lift_split … HVW2 d (i - e + 1)) -HVW2 [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie
+    #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O /3 width=9/
+  ]
+| #a #I #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
+  elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=5/
+| #I #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHV12 … HLK … HWV1) -V1
+  elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5/
+| #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #X #H
+  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHU1 (K.ⓓW1) … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
+  elim (lift_div_le … HU2 … HTU) -U // /3 width=5/
+| #L #V #U1 #U2 #_ #IHU12 #K #d #e #HLK #X #H
+  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3/
+| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #K #d #e #HLK #X #HX
+  elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
+  elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
+  elim (IHV12 … HLK … HV01) -V1
+  elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1/ /3 width=5/
+| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #d #e #HLK #X #HX
+  elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
+  elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
+  elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
+  elim (IHT12 (K.ⓓW0) … HT01) -T1 /2 width=1/ #T3 #HT32 #HT03
+  elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
+  elim (lift_trans_le … HV3 … HV2 ?) -V // #V #HV3 #HV2
+  @ex2_intro [2: /3 width=2/ | skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
+]
+qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fsup_cpx_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+                      ∀U2. ⦃h, L2⦄ ⊢ T2 ➡[g] U2 →
+                      ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
+#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2,3,4,5: /3 width=5/ ]
+[ #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+  elim (IHT12 … HTU2) -IHT12 -HTU2 #T #HT1 #HT2
+  elim (lift_total T d e) #U #HTU
+  lapply (cpx_lift … HT1 … HLK1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+| #I #L1 #V2 #U2 #HVU2
+  elim (lift_total U2 0 1) /4 width=9/
+]
+qed-.
+
+lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+                       ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
+                       ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
+/3 width=4 by fsup_cpx_trans, ssta_cpx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma
new file mode 100644
index 000000000..8460d99ce
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma
@@ -0,0 +1,73 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lpr.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+definition lpx: ∀h. sd h → relation lenv ≝ λh,g. lpx_sn (cpx h g). 
+
+interpretation "extended parallel reduction (local environment, sn variant)"
+   'PRedSn h g L1 L2 = (lpx h g L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpx_inv_atom1: ∀h,g,L2. ⦃h, ⋆⦄ ⊢ ➡[g] L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+lemma lpx_inv_pair1: ∀h,g,I,K1,V1,L2. ⦃h, K1.ⓑ{I}V1⦄ ⊢ ➡[g] L2 →
+                     ∃∃K2,V2. ⦃h, K1⦄ ⊢ ➡[g] K2 & ⦃h, K1⦄ ⊢ V1 ➡[g] V2 &
+                             L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+lemma lpx_inv_atom2: ∀h,g,L1.  ⦃h, L1⦄ ⊢ ➡[g] ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpx_inv_pair2: ∀h,g,I,L1,K2,V2.  ⦃h, L1⦄ ⊢ ➡[g] K2.ⓑ{I}V2 →
+                     ∃∃K1,V1. ⦃h, K1⦄ ⊢ ➡[g] K2 & ⦃h, K1⦄ ⊢ V1 ➡[g] V2 &
+                             L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_refl: ∀h,g,L.  ⦃h, L⦄ ⊢ ➡[g] L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpx_pair: ∀h,g,I,K1,K2,V1,V2. ⦃h, K1⦄ ⊢ ➡[g] K2 → ⦃h, K1⦄ ⊢ V1 ➡[g] V2 →
+                ⦃h, K1.ⓑ{I}V1⦄ ⊢ ➡[g] K2.ⓑ{I}V2.
+/2 width=1/ qed.
+
+lemma lpx_append: ∀h,g,K1,K2. ⦃h, K1⦄ ⊢ ➡[g] K2 → ∀L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 →
+                  ⦃h, L1 @@ K1⦄ ⊢ ➡[g] L2 @@ K2.
+/3 width=1 by lpx_sn_append, cpx_append/ qed.
+
+lemma lpr_lpx: ∀h,g,L1,L2. L1 ⊢ ➡ L2 → ⦃h, L1⦄ ⊢ ➡[g] L2.
+#h #g #L1 #L2 #H elim H -L1 -L2 // /3 width=1/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_fwd_length: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lpx_fwd_append1: ∀h,g,K1,L1,L. ⦃h, K1 @@ L1⦄ ⊢ ➡[g] L →
+                       ∃∃K2,L2. ⦃h, K1⦄ ⊢ ➡[g] K2 & L = K2 @@ L2.
+/2 width=2 by lpx_sn_fwd_append1/ qed-.
+
+lemma lpx_fwd_append2: ∀h,g,L,K2,L2. ⦃h, L⦄ ⊢ ➡[g] K2 @@ L2 →
+                       ∃∃K1,L1. ⦃h, K1⦄ ⊢ ➡[g] K2 & L = K1 @@ L1.
+/2 width=2 by lpx_sn_fwd_append2/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
similarity index 70%
rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_aaa.ma
rename to matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
index 3c59a7873..3863f7bb5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
@@ -14,38 +14,38 @@
 
 include "basic_2/static/aaa_lift.ma".
 include "basic_2/static/lsuba_aaa.ma".
-include "basic_2/reduction/lpr_ldrop.ma".
+include "basic_2/reduction/lpx_ldrop.ma".
 
 (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
 
 (* Properties on atomic arity assignment for terms **************************)
 
-lemma aaa_cpr_lpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. L1 ⊢ T1 ➡ T2 →
-                        ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T2 ⁝ A.
-#L1 #T1 #A #H elim H -L1 -T1 -A
+lemma aaa_cpx_lpx_conf: ∀h,g,L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. ⦃h, L1⦄ ⊢ T1 ➡[g] T2 →
+                        ∀L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → L2 ⊢ T2 ⁝ A.
+#h #g #L1 #T1 #A #H elim H -L1 -T1 -A
 [ #L1 #k #X #H
-  >(cpr_inv_sort1 … H) -H //
+  elim (cpx_inv_sort1 … H) -H // * //
 | #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12
-  elim (cpr_inv_lref1 … H) -H
+  elim (cpx_inv_lref1 … H) -H
   [ #H destruct
-    elim (lpr_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
-    elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
-  | * #Y #Z #V2 #H #HV12 #HV2
+    elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
+    elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
+  | * #J #Y #Z #V2 #H #HV12 #HV2
     lapply (ldrop_mono … H … HLK1) -H #H destruct
-    elim (lpr_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
-    elim (lpr_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
+    elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
+    elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
     lapply (ldrop_fwd_ldrop2 … HLK2) -V0 /3 width=7/
   ]
 | #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
-  elim (cpr_inv_abbr1 … H) -H *
+  elim (cpx_inv_abbr1 … H) -H *
   [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2/
   | #T2 #HT12 #HT2 #H destruct -IHV1
     @(aaa_inv_lift (L2.ⓓV1) … HT2) -HT2 /2 width=1/ /3 width=1/
   ]
 | #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
-  elim (cpr_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=1/
+  elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=1/
 | #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
-  elim (cpr_inv_appl1 … H) -H *
+  elim (cpx_inv_appl1 … H) -H *
   [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3/
   | #b #V2 #W1 #U1 #U2 #HV12 #HU12 #H1 #H2 destruct
     lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
@@ -58,15 +58,21 @@ lemma aaa_cpr_lpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. L1 ⊢ T1 ➡ T2
     elim (aaa_inv_abbr … H) -H /3 width=3/
   ]
 | #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
-  elim (cpr_inv_cast1 … H) -H
+  elim (cpx_inv_cast1 … H) -H
   [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1/
   | -IHV1 /2 width=1/
   ]
 ]
 qed-.
 
+lemma aaa_cpx_conf: ∀h,g,L,T1,A. L ⊢ T1 ⁝ A → ∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → L ⊢ T2 ⁝ A.
+/2 width=7 by aaa_cpx_lpx_conf/ qed-.
+
+lemma aaa_lpx_conf: ∀h,g,L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → L2 ⊢ T ⁝ A.
+/2 width=7 by aaa_cpx_lpx_conf/ qed-.
+
 lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ⁝ A.
-/2 width=5 by aaa_cpr_lpr_conf/ qed-.
+/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-.
 
 lemma aaa_lpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A.
-/2 width=5 by aaa_cpr_lpr_conf/ qed-.
+/3 width=5 by aaa_lpx_conf, lpr_lpx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
new file mode 100644
index 000000000..57459d1a7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/ldrop_lpx_sn.ma".
+include "basic_2/reduction/cpx_lift.ma".
+include "basic_2/reduction/lpx.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpx_ldrop_conf: ∀h,g. dropable_sn (lpx h g).
+/3 width=5 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
+
+lemma ldrop_lpx_trans: ∀h,g. dedropable_sn (lpx h g).
+/3 width=9 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
+
+lemma lpx_ldrop_trans_O1: ∀h,g. dropable_dx (lpx h g).
+/2 width=3 by lpx_sn_dropable/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
index 16fbeb128..a964988d7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
@@ -18,7 +18,7 @@ include "basic_2/relocation/ldrop.ma".
 (* SUPCLOSURE ***************************************************************)
 
 inductive fsup: bi_relation lenv term ≝
-| fsup_lref   : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
+| fsup_lref_O : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
 | fsup_pair_sn: ∀I,L,V,T. fsup L (②{I}V.T) L V
 | fsup_bind_dx: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
 | fsup_flat_dx: ∀I,L,V,T.   fsup L (ⓕ{I}V.T) L T
@@ -55,7 +55,8 @@ lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1
 @(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/
 qed-.
 
-fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀i. T1 = #i → |L2| < |L1|.
+fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+                                ∀i. T1 = #i → |L2| < |L1|.
 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
 [5: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
     lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma
index 9400a84d7..2891cd685 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma
@@ -16,17 +16,55 @@ include "basic_2/relocation/fsup.ma".
 
 (* OPTIONAL SUPCLOSURE ******************************************************)
 
-definition fsupq: bi_relation lenv term ≝ bi_RC … fsup.
+inductive fsupq: bi_relation lenv term ≝
+| fsupq_refl   : ∀L,T. fsupq L T L T
+| fsupq_lref_O : ∀I,L,V. fsupq (L.ⓑ{I}V) (#0) L V
+| fsupq_pair_sn: ∀I,L,V,T. fsupq L (②{I}V.T) L V
+| fsupq_bind_dx: ∀a,I,L,V,T. fsupq L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
+| fsupq_flat_dx: ∀I,L,V,T.   fsupq L (ⓕ{I}V.T) L T
+| fsupq_ldrop  : ∀L1,K1,K2,T1,T2,U1,d,e.
+                ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
+                fsupq K1 T1 K2 T2 → fsupq L1 U1 K2 T2
+.
 
 interpretation
    "optional structural successor (closure)"
-   'SupTermOpt L1 T1 L2 T2 = (fsup L1 T1 L2 T2).
+   'SupTermOpt L1 T1 L2 T2 = (fsupq L1 T1 L2 T2).
 
 (* Basic properties *********************************************************)
 
-lemma fsupq_refl: bi_reflexive … fsupq.
-/2 width=1/ qed.
-
 lemma fsup_fsupq: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄.
-/2 width=1/ qed.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=7/ qed.
+
+(* Basic properties *********************************************************)
+
+lemma fsupq_lref_S_lt: ∀I,L,K,V,T,i. 0 < i → ⦃L, #(i-1)⦄ ⊃⸮ ⦃K, T⦄ → ⦃L.ⓑ{I}V, #i⦄ ⊃⸮ ⦃K, T⦄.
+/3 width=7/ qed.
+
+lemma fsupq_lref: ∀I,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃L, #i⦄ ⊃⸮ ⦃K, V⦄.
+/3 width=2/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fsupq_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // [1,2,3: /2 width=1/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12
+lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1
+lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1
+@(transitive_le … IHT12) -IHT12 /2 width=1/
+qed-.
+
+fact fsupq_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ →
+                                 ∀i. T1 = #i → |L2| ≤ |L1|.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 //
+[ #a #I #L #V #T #j #H destruct
+| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
+  lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+  elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
+  @(transitive_le … HLK1) /2 width=2/
+]
+qed-.
 
+lemma fsupq_fwd_length_lref1: ∀L1,L2,T2,i. ⦃L1, #i⦄ ⊃⸮ ⦃L2, T2⦄ → |L2| ≤ |L1|.
+/2 width=5 by fsupq_fwd_length_lref1_aux/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma
index 72df7717e..7c31b884f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma
@@ -22,6 +22,9 @@ record sh: Type[0] ≝ {
    next_lt: ∀k. k < next k (* strict monotonicity condition *)
 }.
 
+definition sh_N: sh ≝ mk_sh S ….
+// qed.
+
 (* Basic properties *********************************************************)
 
 lemma nexts_le: ∀h,k,l. k ≤ (next h)^l k.
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 799c4c950..7b85ff25e 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
@@ -109,12 +109,17 @@ table {
    ]
    class "water"
    [ { "reduction" * } {
+        [ { "context-sensitive extended reduction" * } {
+             [ "lpx ( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpx_ldrop" + "lpx_aaa" * ]
+             [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpx_lift" * ]
+          }
+        ]
         [ { "context-sensitive normal forms" * } {
              [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_liftt" + "cnf_crf" + "cnf_cif" * ]
           }
         ]
         [ { "context-sensitive reduction" * } {
-             [ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_lpss" + "lpr_aaa" + "lpr_lpr" * ]
+             [ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_lpss" + "lpr_lpr" * ]
              [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cif" * ]
           }
         ]
@@ -195,7 +200,7 @@ table {
    class "orange"
    [ { "relocation" * } {
         [ { "structural successor for closures" * } {
-             [ "fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )" * ]
+             [ "fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )" "fsupq ( ⦃?,?⦄ ⊃⸮ ⦃?,?⦄ )" * ]
           }
         ]
         [ { "global env. slicing" * } {
-- 
2.39.5