From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 19 Jun 2013 15:01:49 +0000 (+0000)
Subject: - partial commit :(
X-Git-Tag: make_still_working~1133
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=80178d6cf86b78bb9fc47f397f4bcfb1fd15a24f;p=helm.git

- partial commit :(
  some work on supclosure and extended reduction ...
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index d3aaae5de..f1f6495bd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -114,18 +114,15 @@ qed.
 lemma cprs_beta_dx: ∀a,L,V1,V2,W,T1,T2.
                     L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 →
                     L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2.
-#a #L #V1 #V2 #W #T1 #T2 #HV12 #H elim H -T2 /3 width=1/
-#T #T2 #_ #HT2 #IHT1
-@(cprs_strap1 … IHT1) -V1 -T1 /3 width=2/
+#a #L #V1 #V2 #W #T1 #T2 #HV12 * -T2 /3 width=1/
+/4 width=6 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_beta/ (**) (* auto too slow without trace *)
 qed.
 
-lemma cprs_theta_dx: ∀a,L,V1,V,V2,W1,T1,T2.
+lemma cprs_theta_dx: ∀a,L,V1,V,V2,W1,W2,T1,T2.
                      L ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → L.ⓓW1 ⊢ T1 ➡* T2 →
-                     ∀W2. L ⊢ W1 ➡ W2 → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
-#a #L #V1 #V #V2 #W1 #T1 #T2 #HV1 #HV2 #H elim H -T2 [ /3 width=3/ ]
-#T #T2 #_ #HT2 #IHT1 #W2 #HW12
-lapply (IHT1 W1 ?) -IHT1 // #HT1
-@(cprs_strap1 … HT1) -HT1 -V -V1 /3 width=1/
+                     L ⊢ W1 ➡ W2 → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
+#a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ]
+/4 width=9 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_theta/ (**) (* auto too slow without trace *)
 qed.
 
 (* Basic inversion lemmas ***************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
new file mode 100644
index 000000000..202d14d14
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma
@@ -0,0 +1,149 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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".
+include "basic_2/computation/cprs.ma".
+
+(* EXTENDED CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS *****************)
+
+definition cpxs: ∀h. sd h → lenv → relation term ≝
+                 λh,g. LTC … (cpx h g).
+
+interpretation "extended context-sensitive parallel computation (term)"
+   'PRedStar h g L T1 T2 = (cpxs h g L T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma cpxs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 →
+                (∀T,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T → ⦃h, L⦄ ⊢ T ➡[g] T2 → R T → R T2) →
+                ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → R T2.
+#h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12
+@(TC_star_ind … HT1 IHT1 … HT12) //
+qed-.
+
+lemma cpxs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 →
+                   (∀T1,T. ⦃h, L⦄ ⊢ T1 ➡[g] T → ⦃h, L⦄ ⊢ T ➡*[g] T2 → R T → R T1) →
+                   ∀T1. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → R T1.
+#h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12
+@(TC_star_ind_dx … HT2 IHT2 … HT12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma cpxs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➡*[g] T.
+/2 width=1/ qed.
+
+lemma cpx_cpxs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+/2 width=1/ qed.
+
+lemma cpxs_strap1: ∀h,g,L,T1,T. ⦃h, L⦄ ⊢ T1 ➡*[g] T →
+                   ∀T2. ⦃h, L⦄ ⊢ T ➡[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+normalize /2 width=3/ qed.
+
+lemma cpxs_strap2: ∀h,g,L,T1,T. ⦃h, L⦄ ⊢ T1 ➡[g] T →
+                   ∀T2. ⦃h, L⦄ ⊢ T ➡*[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+normalize /2 width=3/ qed.
+
+lemma cprs_cpxs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/
+qed.
+
+lemma cpxs_bind_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 →
+                    ∀I,T1,T2. ⦃h, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[g] T2 →
+                    ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2.
+#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1
+/3 width=1/ /3 width=3/
+qed.
+
+lemma cpxs_flat_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 →
+                    ∀T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 →
+                    ∀I. ⦃h, L⦄ ⊢ ⓕ{I} V1. T1 ➡*[g] ⓕ{I} V2. T2.
+#h #g #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2 /3 width=1/ /3 width=5/
+qed.
+
+lemma cpxs_flat_sn: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 →
+                    ∀V1,V2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 →
+                    ∀I. ⦃h, L⦄ ⊢ ⓕ{I} V1. T1 ➡*[g] ⓕ{I} V2. T2.
+#h #g #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2 /3 width=1/ /3 width=5/
+qed.
+
+lemma cpxs_zeta: ∀h,g,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
+                 ⦃h, L.ⓓV⦄ ⊢ T1 ➡*[g] T → ⦃h, L⦄ ⊢ +ⓓV.T1 ➡*[g] T2.
+#h #g #L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/
+qed.
+
+lemma cpxs_tau: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → ∀V. ⦃h, L⦄ ⊢ ⓝV.T1 ➡*[g] T2.
+#h #g #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/
+qed.
+
+lemma cpxs_beta_dx: ∀h,g,a,L,V1,V2,W,T1,T2.
+                    ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 →
+                    ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W.T1 ➡*[g] ⓓ{a}V2.T2.
+#h #g #a #L #V1 #V2 #W #T1 #T2 #HV12 * -T2 /3 width=1/
+/4 width=6 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ (**) (* auto too slow without trace *)
+qed.
+
+lemma cpxs_theta_dx: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2.
+                     ⦃h, L⦄ ⊢ V1 ➡[g] V → ⇧[0, 1] V ≡ V2 → ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 →
+                     ⦃h, L⦄ ⊢ W1 ➡[g] W2 → ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2.
+#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ]
+/4 width=9 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/ (**) (* auto too slow without trace *)
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cpxs_inv_sort1: ∀h,g,L,U2,k. ⦃h, L⦄ ⊢ ⋆k ➡*[g] U2 →
+                      ∃∃n,l. deg h g k (n+l) & U2 = ⋆((next h)^n k).
+#h #g #L #U2 #k #H @(cpxs_ind … H) -U2
+[ elim (deg_total h g k) #l #Hkl
+  @(ex2_2_intro … 0 … Hkl) -Hkl //
+| #U #U2 #_ #HU2 * #n #l #Hknl #H destruct
+  elim (cpx_inv_sort1 … HU2) -HU2
+  [ #H destruct /2 width=4/
+  | * #l0 #Hkl0 #H destruct -l
+    @(ex2_2_intro … (n+1) l0) /2 width=1/ >iter_SO //
+  ]
+]
+qed-.
+
+lemma cpxs_inv_appl1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡*[g] U2 →
+                      ∨∨ ∃∃V2,T2.       ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 &
+                                        U2 = ⓐV2. T2
+                       | ∃∃a,V2,W,T.    ⦃h, L⦄ ⊢ V1 ➡*[g] V2 &
+                                        ⦃h, L⦄ ⊢ T1 ➡*[g] ⓛ{a}W.T & ⦃h, L⦄ ⊢ ⓓ{a}V2.T ➡*[g] U2
+                       | ∃∃a,V0,V2,V,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V0 & ⇧[0,1] V0 ≡ V2 &
+                                        ⦃h, L⦄ ⊢ T1 ➡*[g] ⓓ{a}V.T & ⦃h, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[g] U2.
+#h #g #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5/ ]
+#U #U2 #_ #HU2 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+  elim (cpx_inv_appl1 … HU2) -HU2 *
+  [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+  | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
+    lapply (cpxs_strap1 … HV10 … HV02) -V0 /5 width=7/
+  | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
+    @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
+  ]
+| /4 width=9/
+| /4 width=11/
+]
+qed-.
+
+lemma cpxs_inv_cast1: ∀h,g,L,W1,T1,U2. ⦃h, L⦄ ⊢ ⓝW1.T1 ➡*[g] U2 → ⦃h, L⦄ ⊢ T1 ➡*[g] U2 ∨
+                      ∃∃W2,T2. ⦃h, L⦄ ⊢ W1 ➡*[g] W2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 & U2 = ⓝW2.T2.
+#h #g #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/
+#U2 #U #_ #HU2 * /3 width=3/ *
+#W #T #HW1 #HT1 #H destruct
+elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3/ *
+#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
new file mode 100644
index 000000000..47d66618b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
@@ -0,0 +1,87 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_lift.ma".
+include "basic_2/computation/cpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Advanced properties ******************************************************)
+
+lemma cpxs_delta: ∀h,g,I,L,K,V,V2,i.
+                  ⇩[0, i] L ≡ K. ⓑ{I}V → ⦃h, K⦄ ⊢ V ➡*[g] V2 →
+                  ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃h, L⦄ ⊢ #i ➡*[g] W2.
+#h #g #I #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=9/ ]
+#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2
+lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpxs_inv_lref1: ∀h,g,L,T2,i. ⦃h, L⦄ ⊢ #i ➡*[g] T2 →
+                      T2 = #i ∨
+                      ∃∃I,K,V1,T1. ⇩[0, i] L ≡ K.ⓑ{I}V1 & ⦃h, K⦄ ⊢ V1 ➡*[g] T1 &
+                                   ⇧[0, i + 1] T1 ≡ T2.
+#h #g #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1/
+#T #T2 #_ #HT2 *
+[ #H destruct
+  elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1/
+  * /4 width=7/
+| * #I #K #V1 #T1 #HLK #HVT1 #HT1
+  lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+  elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=7/
+]
+qed-.
+
+(* Relocation properties ****************************************************)
+
+(* Basic_1: was: pr3_lift *)
+lemma cpxs_lift: ∀h,g. l_liftable (cpxs h g).
+/3 width=9/ qed.
+
+(* Basic_1: was: pr3_gen_lift *)
+lemma cpxs_inv_lift1: ∀h,g. l_deliftable_sn (cpxs h g).
+/3 width=5 by l_deliftable_sn_LTC, cpx_inv_lift1/
+qed-.
+
+(* Properties on supclosure *************************************************)
+
+include "basic_2/substitution/fsups.ma".
+
+lemma fsupq_cpxs_trans: ∀h,g,L1,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 ➡*[g] U2 →
+                        ∀T1. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ →
+                        ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡*[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄.
+#h #g #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 [ (* /3 width=3/ *) |
+#T #T2 #HT2 #_ #IHTU2 #T1 #HT1
+elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2
+elim (IHTU2 … HT2) -T2 /3 width=3/
+
+
+(*
+ 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-.
+*)
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
index c8c98ecfc..a0e62745a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma
@@ -154,6 +154,10 @@ notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃⸮ break ⦃ term 46 L
    non associative with precedence 45
    for @{ 'SupTermOpt $L1 $T1 $L2 $T2 }.
 
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃⊃⸮ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'SupTermOptAlt $L1 $T1 $L2 $T2 }.
+
 notation "hvbox( L ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )"
    non associative with precedence 45
    for @{ 'ICM $L $T $k }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index 935d5c7b0..33063d819 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
@@ -109,10 +109,10 @@ lemma cpx_inv_atom1: ∀h,g,J,L,T2. ⦃h, L⦄ ⊢ ⓪{J} ➡[g] T2 →
 /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).
+                     ∃∃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/
+[ #k0 #l0 #Hkl0 #H1 #H2 destruct /3 width=4/
 | #I #K #V #V2 #i #_ #_ #_ #H destruct
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
index 427c0a28b..325fcbf82 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -111,20 +111,30 @@ 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
+lemma fsupq_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 [1: /2 width=3/ |3,4,5: /3 width=3/ ]
+[ #I #L1 #V2 #U2 #HVU2
+  elim (lift_total U2 0 1) /4 width=9/
+| #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 fsupq_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 fsupq_cpx_trans, ssta_cpx/ qed-.
+
+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⦄.
+/3 width=3 by fsupq_cpx_trans, fsup_fsupq/ 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-.
+/3 width=4 by fsupq_ssta_trans, fsup_fsupq/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
index a964988d7..d10d9d28b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma
@@ -18,13 +18,15 @@ include "basic_2/relocation/ldrop.ma".
 (* SUPCLOSURE ***************************************************************)
 
 inductive fsup: bi_relation lenv term ≝
-| 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
-| fsup_ldrop  : ∀L1,K1,K2,T1,T2,U1,d,e.
-                ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
-                fsup K1 T1 K2 T2 → fsup L1 U1 K2 T2
+| 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
+| fsup_ldrop_lt: ∀L,K,T,U,d,e.
+                 ⇩[d, e] L ≡ K → ⇧[d, e] T ≡ U → |K| < |L| → fsup L U K T
+| fsup_ldrop   : ∀L1,K1,K2,T1,T2,U1,d,e.
+                 ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
+                 fsup K1 T1 K2 T2 → fsup L1 U1 K2 T2
 .
 
 interpretation
@@ -49,20 +51,26 @@ qed.
 
 lemma fsup_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 //
-#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
-@(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/
+[ #L #K #T #U #d #e #HLK #HTU #HKL
+  lapply (ldrop_fwd_lw_lt … HLK HKL) -HKL -HLK #HKL
+  lapply (lift_fwd_tw … HTU) -d -e #H
+  normalize in ⊢ (?%%); /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
+  @(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|.
 #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
+[1,5:  normalize //
+|3: #a
+|6: #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
     @(lt_to_le_to_lt … HLK1) /2 width=2/
-| normalize // |3: #a
 ] #I #L #V #T #j #H destruct
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index 7d3b3b0ce..f51640fa1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -296,6 +296,29 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → |L2| = |L1| - e.
 ]
 qed-.
 
+lemma ldrop_fwd_lw_eq: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
+                       |L1| = |L2| → ♯{L2} = ♯{L1}.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e //
+[ #L1 #L2 #I #V #e #HL12 #_
+  lapply (ldrop_fwd_O1_length … HL12) -HL12 #HL21 >HL21 -HL21 normalize #H -I
+  lapply (discr_plus_xy_minus_xz … H) -e #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #HL12 normalize in ⊢ (??%%→??%%); #H -I 
+  >(lift_fwd_tw … HV21) -V2 /3 width=1 by eq_f2/ (**) (* auto is a bit slow without trace *)
+]
+qed-.
+
+lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
+                      |L2| < |L1| → ♯{L2} < ♯{L1}.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e //
+[ #L #I #V #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V #e #HL12 #_ #_
+  lapply (ldrop_fwd_lw … HL12) -HL12 #HL12
+  @(le_to_lt_to_lt … HL12) -HL12 //
+| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 normalize in ⊢ (?%%→?%%); #H -I
+  >(lift_fwd_tw … HV21) -V2 /4 width=2 by lt_minus_to_plus, lt_plus_to_lt_l/ (**) (* auto too slow without trace *)
+]
+qed-.
+
 (* Basic_1: removed theorems 50:
             drop_ctail drop_skip_flat
             cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
index d6737a8ba..79d9f0740 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
@@ -100,6 +100,13 @@ lapply (deg_mono … H1 H2) -H1 -H2 #H
 <(associative_plus l 1 1) >H <plus_minus_m_m // /2 width=3 by transitive_le/
 qed.
 
+lemma deg_prec: ∀h,g,k,l,l0. deg h g ((next h)^l k) (l0+1) → deg h g k (l+l0+1).
+#h #g #k #l @(nat_ind_plus … l) -l //
+#l #IHl #l0 >iter_SO #H
+lapply (deg_pred … H) -H <(associative_plus l0 1 1) #H
+lapply (IHl … H) -IHl -H //
+qed.
+
 lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
 #h #k #l <plus_n_Sm <plus_n_Sm //
 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 7b85ff25e..5d5b58611 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
@@ -83,6 +83,10 @@ table {
              [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ]
           }
         ]
+        [ { "context-sensitive extended computation" * } {
+             [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )" "cpxs_lift" * ]
+          }
+        ]
         [ { "weakly normalizing computation" * } {
              [ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ]
           }
diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 7bd51c318..249bd274e 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -164,7 +164,7 @@ lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
 // qed. 
 
 theorem times_n_1 : ∀n:nat. n = n * 1.
-#n // qed.
+// qed.
 
 theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
 // qed.
@@ -187,6 +187,13 @@ theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
 lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
 // qed.
 
+lemma discr_plus_xy_minus_xz: ∀x,z,y. x + y = x - z → y = 0.
+#x elim x -x // #x #IHx * normalize
+[ #y #H @(IHx 0) <minus_n_O /2 width=1/
+| #z #y >plus_n_Sm #H lapply (IHx … H) -x -z #H destruct
+]
+qed-.
+
 (* Negated equalities *******************************************************)
 
 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.