From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Wed, 20 Mar 2019 11:30:38 +0000 (+0100)
Subject: update in ground_2 static_2 basic_2
X-Git-Tag: make_still_working~255
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a67fc50ccfda64377e2c94c18c3a0d9265f651db

update in ground_2 static_2 basic_2

+ whd normal forms for terms with arity
+ positive abbreviations are not whd normal forms
+ minor additions
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_4.ma
new file mode 100644
index 000000000..05f4ee9c6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_4.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ [ break term 46 h ] 𝐖𝐇 ⦃ break term 46 T ⦄ )"
+   non associative with precedence 45
+   for @{ 'PRedTyWHead $h $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_5.ma
deleted file mode 100644
index bd6c4268c..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_5.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ [ break term 46 h, break term 46 o ] 𝐖𝐇 ⦃ break term 46 T ⦄ )"
-   non associative with precedence 45
-   for @{ 'PRedTyWHead $h $o $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma
new file mode 100644
index 000000000..223efe3e0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma
@@ -0,0 +1,76 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_transition/cpr_tdeq.ma".
+include "basic_2/rt_transition/cwhx_drops.ma".
+include "basic_2/rt_transition/cwhx_rdeq.ma".
+include "basic_2/rt_computation/fsb_aaa.ma".
+include "basic_2/rt_computation/cpms_cpms.ma".
+include "basic_2/rt_computation/cpms_fpbg.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Properties with whd normality for unbound rt-transition ******************)
+
+lemma aaa_cpms_cwhx (h) (G) (L):
+                    ∀T1,A. ⦃G,L⦄ ⊢ T1 ⁝ A →
+                    ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄.
+#h #G #L #T1 #A #H
+letin o ≝ (sd_O h)
+@(aaa_ind_fpbg … o … H) -G -L -T1 -A
+#G #L #T1 #A * -G -L -T1 -A
+[ #G #L #s #_ /2 width=4 by cwhx_sort, ex2_2_intro/
+| * #G #K #V1 #A #_ #IH -A
+  elim (IH … G K V1) [2,4: /3 width=1 by fpb_fpbg, fpb_fqu, fqu_lref_O/ ] -IH #n #V2 #HV12 #HV2
+  elim (lifts_total … V2 (𝐔❴1❵)) #T2 #HVT2
+  /5 width=10 by cpms_ell, cpms_delta, cwhx_lifts, drops_refl, drops_drop, ex2_2_intro/
+| #I #G #K #A #i #_ #IH -A
+  elim (IH … G K (#i)) [| /3 width=1 by fpb_fpbg, fpb_fqu/ ] -IH #n #V2 #HV12 #HV2
+  elim (lifts_total … V2 (𝐔❴1❵)) #T2 #HVT2
+  /5 width=10 by cpms_lref, cwhx_lifts, drops_refl, drops_drop, ex2_2_intro/
+| * #G #L #V #T1 #B #A #_ #_ #IH -B -A
+  [ elim (cpr_abbr_pos h o G L V T1) #T0 #HT10 #HnT10
+    elim (IH G L T0) -IH [| /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HnT10 #n #T2 #HT02 #HT2
+    /3 width=5 by cpms_step_sn, ex2_2_intro/
+  | elim (IH … G (L.ⓓV) T1) -IH [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_bind_dx/ ] #n #T2 #HT12 #HT2
+    /3 width=5 by cwhx_ldef, cpms_bind_dx, ex2_2_intro/
+  ]
+| #p #G #L #W #T1 #B #A #_ #_ #_ -B -A
+  /2 width=5 by cwhx_abst, ex2_2_intro/
+| #G #L #V #T1 #B #A #_ #HT1 #IH
+  elim (IH … G L T1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #n1 #T2 #HT12 #HT2
+  elim (tdeq_dec h o T1 T2) [ -n1 #HT12 | -HT2 #HnT12 ]
+  [ lapply (tdeq_cwhx_trans … HT2 … HT12) -T2
+    @(insert_eq_0 … L) #Y @(insert_eq_0 … T1) #X * -Y -X
+    [ #L0 #s0 #H1 #H2 destruct -IH
+      lapply (aaa_inv_sort … HT1) -HT1 #H destruct
+    | #p #L0 #W0 #T0 #H1 #H2 destruct -HT1
+      elim (IH G L0 (ⓓ{p}ⓝW0.V.T0)) -IH [ /4 width=5 by cpms_step_sn, cpm_beta, ex2_2_intro/ ]
+      @fpb_fpbg @fpb_cpx [ /2 width=1 by cpx_beta/ ] #H
+      elim (tdeq_inv_pair … H) -H #H #_ #_ destruct
+    | #L0 #V0 #T0 #_ #H1 #H2 destruct -HT1
+      elim (lifts_total V (𝐔❴1❵)) #W #HVW
+      elim (IH G L0 (-ⓓV0.ⓐW.T0)) -IH [ /4 width=5 by cpms_step_sn, cpm_theta, ex2_2_intro/ ]
+      @fpb_fpbg @fpb_cpx [ /2 width=3 by cpx_theta/ ] #H
+      elim (tdeq_inv_pair … H) -H #H #_ #_ destruct
+    ]
+  | elim (IH G L (ⓐV.T2)) -IH [ /4 width=5 by cpms_trans, cpms_appl_dx, ex2_2_intro/ ]
+    @(cpms_tdneq_fwd_fpbg … n1) [ /2 width=3 by cpms_appl_dx/ ] #H
+    elim (tdeq_inv_pair … H) -H #_ #_ #H /2 width=1 by/
+  ]
+| #G #L #U #T1 #A #_ #_ #IH -A
+  elim (IH … G L T1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #n #T2 #HT12 #HT2
+  /3 width=4 by cpms_eps, ex2_2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
index 7584e81c9..8c0c3204e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
@@ -13,13 +13,17 @@
 (**************************************************************************)
 
 include "basic_2/rt_computation/fpbg_fqup.ma".
-include "basic_2/rt_computation/fpbg_fpbs.ma".
+include "basic_2/rt_computation/fpbg_cpxs.ma".
 include "basic_2/rt_computation/cpms_fpbs.ma".
 
 (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
 
 (* Forward lemmas with proper parallel rst-computation for closures *********)
 
+lemma cpms_tdneq_fwd_fpbg (h) (o) (n): ∀G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 →
+                                       (T1 ≛[h,o] T2 → ⊥) → ⦃G,L,T1⦄ >[h,o] ⦃G,L,T2⦄.
+/3 width=2 by cpms_fwd_cpxs, cpxs_tdneq_fpbg/ qed-.
+
 lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T⦄ →
                                    ∀T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
 /3 width=5 by fpbg_fpbs_trans, cpms_fwd_fpbs/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma
new file mode 100644
index 000000000..326de686e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/relocation/lifts_tdeq.ma".
+include "basic_2/rt_transition/cpx_drops_basic.ma".
+include "basic_2/rt_transition/cnx.ma".
+
+(* NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ********)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cnx_inv_abbr_pos (h) (o) (G) (L): ∀V,T.  ⦃G,L⦄ ⊢ ⬈[h,o] 𝐍⦃+ⓓV.T⦄ → ⊥.
+#h #o #G #L #V #U1 #H
+elim (cpx_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2
+elim (tdeq_dec h o U1 U2) #HnU12 [ -HU12 | -HTU2 ]
+[ elim (tdeq_inv_lifts_dx … HnU12 … HTU2) -U2 #T1 #HTU1 #_ -T2
+  lapply (H T1 ?) -H [ /2 width=3 by cpx_zeta/ ] #H
+  /2 width=9 by tdeq_lifts_inv_pair_sn/
+| lapply (H (+ⓓV.U2) ?) -H [ /2 width=1 by cpx_bind/ ] -HU12 #H
+  elim (tdeq_inv_pair … H) -H #_ #_ /2 width=1 by/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops_basic.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops_basic.ma
new file mode 100644
index 000000000..705031ffd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops_basic.ma
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/relocation/lifts_basic.ma".
+include "basic_2/rt_transition/cpm_drops.ma".
+include "basic_2/rt_transition/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
+
+(* Properties with basic relocation *****************************************)
+
+lemma cpr_subst (h) (G) (L) (U1) (i):
+                ∀K,V. ⬇*[i] L ≘ K.ⓓV →
+                ∃∃U2,T2. ⦃G, L⦄ ⊢ U1 ➡[h] U2 & ⬆[i,1] T2 ≘ U2.
+#h #G #L #U1 @(fqup_wf_ind_eq (Ⓣ) … G L U1) -G -L -U1
+#G0 #L0 #U0 #IH #G #L * *
+[ #s #HG #HL #HT #i #K #V #_ destruct -IH
+  /2 width=4 by lifts_sort, ex2_2_intro/
+| #j #HG #HL #HT #i #K #V #HLK destruct -IH
+  elim (lt_or_eq_or_gt i j) #Hij
+  [ /3 width=4 by lifts_lref_ge_minus, cpr_refl, ex2_2_intro/
+  | elim (lifts_total V (𝐔❴↑i❵)) #U2 #HU2
+    elim (lifts_split_trans … HU2 (𝐔❴i❵) (𝐁❴i,1❵)) [2: @(after_basic_rc i 0) ]
+    /3 width=7 by cpm_delta_drops, ex2_2_intro/
+  | /3 width=4 by lifts_lref_lt, cpr_refl, ex2_2_intro/
+  ]
+| #l #HG #HL #HT #i #K #V #_ destruct -IH
+  /2 width=4 by lifts_gref, ex2_2_intro/
+| #p #J #W1 #U1 #HG #HL #HT #i #K #V #HLK destruct
+  elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2
+  elim (IH G (L.ⓑ{J}W1) U1 … (↑i)) [|*: /3 width=4 by drops_drop/ ] #U2 #T2 #HU12 #HTU2
+  /3 width=9 by cpm_bind, lifts_bind, ex2_2_intro/
+| #J #W1 #U1 #HG #HL #HT #i #K #V #HLK destruct
+  elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2
+  elim (IH G L U1 … HLK) [| // ] #U2 #T2 #HU12 #HTU2
+  /3 width=8 by cpr_flat, lifts_flat, ex2_2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma
new file mode 100644
index 000000000..f4a899d0d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/relocation/lifts_tdeq.ma".
+include "basic_2/rt_transition/cpr_drops_basic.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
+
+(* Properties with context-free degree-based equivalence ********************)
+
+lemma cpr_abbr_pos (h) (o) (G) (L) (V) (T1):
+                   ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡[h] T2 & (+ⓓV.T1 ≛[h, o] T2 → ⊥).
+#h #o #G #L #V #U1
+elim (cpr_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2
+elim (tdeq_dec h o U1 U2) [ -HU12 #HU12 | -HTU2 #HnU12 ]
+[ elim (tdeq_inv_lifts_dx … HU12 … HTU2) -U2 #T1 #HTU1 #_ -T2
+  /3 width=9 by cpm_zeta, tdeq_lifts_inv_pair_sn, ex2_intro/
+| @(ex2_intro … (+ⓓV.U2)) [ /2 width=1 by cpm_bind/ ] -HU12 #H
+  elim (tdeq_inv_pair … H) -H #_ #_ /2 width=1 by/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops_basic.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops_basic.ma
new file mode 100644
index 000000000..09b998bae
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops_basic.ma
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/relocation/lifts_basic.ma".
+include "basic_2/rt_transition/cpx_drops.ma".
+
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Properties with basic relocation *****************************************)
+
+lemma cpx_subst (h) (G) (L) (U1) (i):
+                ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V →
+                ∃∃U2,T2. ⦃G, L⦄ ⊢ U1 ⬈[h] U2 & ⬆[i,1] T2 ≘ U2.
+#h #G #L #U1 @(fqup_wf_ind_eq (Ⓣ) … G L U1) -G -L -U1
+#G0 #L0 #U0 #IH #G #L * *
+[ #s #HG #HL #HT #i #I #K #V #_ destruct -IH
+  /2 width=4 by lifts_sort, ex2_2_intro/
+| #j #HG #HL #HT #i #I #K #V #HLK destruct -IH
+  elim (lt_or_eq_or_gt i j) #Hij
+  [ /3 width=4 by lifts_lref_ge_minus, cpx_refl, ex2_2_intro/
+  | elim (lifts_total V (𝐔❴↑i❵)) #U2 #HU2
+    elim (lifts_split_trans … HU2 (𝐔❴i❵) (𝐁❴i,1❵)) [2: @(after_basic_rc i 0) ]
+    /3 width=7 by cpx_delta_drops, ex2_2_intro/
+  | /3 width=4 by lifts_lref_lt, cpx_refl, ex2_2_intro/
+  ]
+| #l #HG #HL #HT #i #I #K #V #_ destruct -IH
+  /2 width=4 by lifts_gref, ex2_2_intro/
+| #p #J #W1 #U1 #HG #HL #HT #i #I #K #V #HLK destruct
+  elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2
+  elim (IH G (L.ⓑ{J}W1) U1 … (↑i)) [|*: /3 width=4 by drops_drop/ ] #U2 #T2 #HU12 #HTU2
+  /3 width=9 by cpx_bind, lifts_bind, ex2_2_intro/
+| #J #W1 #U1 #HG #HL #HT #i #I #K #V #HLK destruct
+  elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2
+  elim (IH G L U1 … HLK) [| // ] #U2 #T2 #HU12 #HTU2
+  /3 width=8 by cpx_flat, lifts_flat, ex2_2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma
index 007c15e3f..0317cc097 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma
@@ -12,63 +12,105 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/predtywhead_5.ma".
-include "static_2/syntax/item_sd.ma".
+include "basic_2/notation/relations/predtywhead_4.ma".
+include "static_2/syntax/item_sh.ma".
 include "static_2/syntax/lenv.ma".
 include "static_2/syntax/genv.ma".
 
 (* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****)
 
-inductive cwhx (h) (o:sd h) (G:genv): relation2 lenv term ≝
-| cwhx_sort: ∀L,s. cwhx h o G L (⋆s)
-| cwhx_abst: ∀p,L,W,T. cwhx h o G L (ⓛ{p}W.T)
-| cwhx_neg : ∀L,V,T. cwhx h o G (L.ⓓV) T → cwhx h o G L (-ⓓV.T)
+inductive cwhx (h:sh) (G:genv): relation2 lenv term ≝
+| cwhx_sort: ∀L,s. cwhx h G L (⋆s)
+| cwhx_abst: ∀p,L,W,T. cwhx h G L (ⓛ{p}W.T)
+| cwhx_ldef: ∀L,V,T. cwhx h G (L.ⓓV) T → cwhx h G L (-ⓓV.T)
 .
 
 interpretation
    "whd normality for unbound context-sensitive parallel rt-transition (term)"
-   'PRedTyWHead h o G L T = (cwhx h o G L T).
+   'PRedTyWHead h G L T = (cwhx h G L T).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact cwhx_inv_lref_aux (h) (o) (G):
-                       ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ →
+fact cwhx_inv_lref_aux (h) (G):
+                       ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
                        ∀i. X = #i → ⊥.
-#h #o #G #Y #X * - X -Y
+#h #G #Y #X * - X -Y
 [ #L #s #i #H destruct
 | #p #L #W #T #i #H destruct
 | #L #V #T #_ #i #H destruct
 ]
 qed-.
 
-lemma cwhx_inv_lref (h) (o) (G):
-                    ∀L,i. ⦃G,L⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃#i⦄ → ⊥.
-/2 width=8 by cwhx_inv_lref_aux/ qed-.
+lemma cwhx_inv_lref (h) (G):
+                    ∀L,i. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃#i⦄ → ⊥.
+/2 width=7 by cwhx_inv_lref_aux/ qed-.
 
-fact cwhx_inv_gref_aux (h) (o) (G):
-                       ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ →
+fact cwhx_inv_gref_aux (h) (G):
+                       ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
                        ∀l. X = §l → ⊥.
-#h #o #G #Y #X * - X -Y
+#h #G #Y #X * - X -Y
 [ #L #s #l #H destruct
 | #p #L #W #T #l #H destruct
 | #L #V #T #_ #l #H destruct
 ]
 qed-.
 
-lemma cwhx_inv_gref (h) (o) (G):
-                    ∀L,l. ⦃G,L⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃§l⦄ → ⊥.
-/2 width=8 by cwhx_inv_gref_aux/ qed-.
+lemma cwhx_inv_gref (h) (G):
+                    ∀L,l. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃§l⦄ → ⊥.
+/2 width=7 by cwhx_inv_gref_aux/ qed-.
 
-fact cwhx_inv_pos_aux (h) (o) (G):
-                      ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ →
-                      ∀W,U. X = +ⓓW.U → ⊥.
-#h #o #G #Y #X * - X -Y
+fact cwhx_inv_abbr_aux (h) (G):
+                       ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
+                       ∀V,T. X = +ⓓV.T → ⊥.
+#h #G #Y #X * - X -Y
 [ #L #s #X1 #X2 #H destruct
 | #p #L #W #T #X1 #X2 #H destruct
 | #L #V #T #_ #X1 #X2 #H destruct
 ]
 qed-.
 
-lemma cwhx_inv_pos (h) (o) (G):
-                   ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃+ⓓV.T⦄ → ⊥.
-/2 width=9 by cwhx_inv_pos_aux/ qed-.
+lemma cwhx_inv_abbr (h) (G):
+                    ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃+ⓓV.T⦄ → ⊥.
+/2 width=8 by cwhx_inv_abbr_aux/ qed-.
+
+fact cwhx_inv_ldef_aux (h) (G):
+                       ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
+                       ∀V,T. X = -ⓓV.T → ⦃G,Y.ⓓV⦄ ⊢ ⬈[h] 𝐖𝐇⦃T⦄.
+#h #G #Y #X * - X -Y
+[ #L #s #X1 #X2 #H destruct
+| #p #L #W #T #X1 #X2 #H destruct
+| #L #V #T #HT #X1 #X2 #H destruct //
+]
+qed-.
+
+lemma cwhx_inv_ldef (h) (G):
+                    ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃-ⓓV.T⦄ → ⦃G,Y.ⓓV⦄ ⊢ ⬈[h] 𝐖𝐇⦃T⦄.
+/2 width=3 by cwhx_inv_ldef_aux/ qed-.
+
+fact cwhx_inv_appl_aux (h) (G):
+                       ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
+                       ∀V,T. X = ⓐV.T → ⊥.
+#h #G #Y #X * - X -Y
+[ #L #s #X1 #X2 #H destruct
+| #p #L #W #T #X1 #X2 #H destruct
+| #L #V #T #_ #X1 #X2 #H destruct
+]
+qed-.
+
+lemma cwhx_inv_appl (h) (G):
+                    ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃ⓐV.T⦄ → ⊥.
+/2 width=8 by cwhx_inv_appl_aux/ qed-.
+
+fact cwhx_inv_cast_aux (h) (G):
+                       ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ →
+                       ∀U,T. X = ⓝU.T → ⊥.
+#h #G #Y #X * - X -Y
+[ #L #s #X1 #X2 #H destruct
+| #p #L #W #T #X1 #X2 #H destruct
+| #L #V #T #_ #X1 #X2 #H destruct
+]
+qed-.
+
+lemma cwhx_inv_cast (h) (G):
+                    ∀Y,U,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃ⓝU.T⦄ → ⊥.
+/2 width=8 by cwhx_inv_cast_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma
new file mode 100644
index 000000000..8ef7b522b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/relocation/drops.ma".
+include "basic_2/rt_transition/cwhx.ma".
+
+(* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****)
+
+(* Properties with generic slicing ******************************************)
+
+lemma cwhx_lifts (h) (G): d_liftable1 … (cwhx h G).
+#h #G #K #T #H elim H -K -T
+[ #K #s #b #f #L #HLK #X #H
+  lapply (lifts_inv_sort1 … H) -H #H destruct //
+| #p #K #V #T #b #f #L #HLK #X #H
+  elim (lifts_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct //
+| #K #V #T #_ #IH #b #f #L #HLK #X #H
+  elim (lifts_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct
+  /5 width=4 by cwhx_ldef, drops_skip, ext2_pair/
+]
+qed-.
+
+(* Inversion lemmas with generic slicing ************************************)
+
+lemma cwhx_inv_lifts (h) (G): d_deliftable1 … (cwhx h G).
+#h #G #L #U #H elim H -L -U
+[ #L #s #b #f #K #HLK #X #H
+  lapply (lifts_inv_sort2 … H) -H #H destruct //
+| #p #L #W #U #b #f #K #HLK #X #H
+  elim (lifts_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct //
+| #L #W #U #_ #IH #b #f #K #HLK #X #H
+  elim (lifts_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct
+  /5 width=4 by cwhx_ldef, drops_skip, ext2_pair/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma
new file mode 100644
index 000000000..884093ad2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/static/rdeq_fqup.ma".
+include "basic_2/rt_transition/cwhx.ma".
+
+(* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****)
+
+(* Properties with degree-based equivalence *********************************)
+
+lemma rdeq_tdeq_cwhx_trans (h) (o) (G):
+                           ∀L2,T2. ⦃G,L2⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄ →
+                           ∀T1. T1 ≛[h,o] T2 →
+                           ∀L1. L1 ≛[h,o,T1] L2 → ⦃G,L1⦄ ⊢ ⬈[h] 𝐖𝐇⦃T1⦄.
+#h #o #G #L2 #T2 #H elim H -L2 -T2
+[ #L2 #s2 #X1 #HX #L1 #HL
+  elim (tdeq_inv_sort2 … HX) -HX #s1 #d #_ #_ #H destruct -s2 -d //
+| #p #L2 #W2 #T2 #X1 #HX #L1 #HL
+  elim (tdeq_inv_pair2 … HX) -HX #W1 #T1 #_ #_ #H destruct -W2 -T2 //
+| #L2 #V2 #T2 #_ #IH #X1 #HX #L1 #HL
+  elim (tdeq_inv_pair2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct
+  elim (rdeq_inv_bind … HL) -HL #HV1 #HT1
+  /5 width=2 by cwhx_ldef, rdeq_bind_repl_dx, ext2_pair/
+]
+qed-.
+
+lemma tdeq_cwhx_trans (h) (o) (G) (L):
+                      ∀T2. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄ →
+                      ∀T1. T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T1⦄.
+/3 width=6 by rdeq_tdeq_cwhx_trans/ 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 850588ce1..bac5d2dd2 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
@@ -61,7 +61,7 @@ table {
           }
         ]
         [ { "t-bound context-sensitive parallel rt-computation" * } {
-             [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
+             [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_cwhx" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
           }
         ]
         [ { "unbound context-sensitive parallel rst-computation" * } {
@@ -92,7 +92,7 @@ table {
         [ { "context-sensitive parallel r-transition" * } {
              [ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ]
              [ [ "for binders" ] "cpr_ext" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ]
-             [ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" + "cpr_cpr" * ]
+             [ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" + "cpr_drops_basic" + "cpr_tdeq" + "cpr_cpr" * ]
           }
         ]
         [ { "t-bound context-sensitive parallel rt-transition" * } {
@@ -100,11 +100,12 @@ table {
           }
         ]
         [ { "unbound context-sensitive parallel rt-transition" * } {
-             [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ]
+             [ [ "whd normal form for terms" ] "cwhx" + "( ⦃?,?⦄ ⊢ ⬈[?] 𝐖𝐇⦃?⦄ )" "cwhx_drops" + "cwhx_rdeq" * ]
+             [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_basic" + "cnx_cnx" * ]
              [ [ "for lenvs on referred entries" ] "rpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_drops" + "rpx_fqup" + "rpx_fsle" + "rpx_rdeq" + "rpx_lpx" + "rpx_rpx" * ]
              [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" "lpx_length" + "lpx_drops" + "lpx_fquq" + "lpx_fsle" + "lpx_rdeq" + "lpx_aaa" * ]
              [ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
-             [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_req" + "cpx_rdeq" + "cpx_fdeq" * ]
+             [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_drops_basic" + "cpx_fqus" + "cpx_lsubr" + "cpx_req" + "cpx_rdeq" + "cpx_fdeq" * ]
           }
         ]
         [ { "bound context-sensitive parallel rt-transition" * } {
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index a29899d45..0574e1757 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -127,6 +127,14 @@ qed-.
 lemma le_plus_to_minus_comm: ∀n,m,p. n ≤ p+m → n-p ≤ m.
 /2 width=1 by le_plus_to_minus/ qed-.
 
+lemma le_inv_S1: ∀m,n. ↑m ≤ n → ∃∃p. m ≤ p & ↑p = n.
+#m *
+[ #H lapply (le_n_O_to_eq … H) -H
+  #H destruct
+| /3 width=3 by monotonic_pred, ex2_intro/
+]
+qed-.
+
 (* Note: this might interfere with nat.ma *)
 lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n.
 #m #n #Hmn #Hm whd >(S_pred … Hm)
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma
new file mode 100644
index 000000000..788d8c24f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground_2/relocation/rtmap_after.ma".
+include "ground_2/relocation/rtmap_basic.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+(* Properties with composition **********************************************)
+
+lemma after_basic_rc (m2,m1,n2,n1):
+                     m1 ≤ m2 → m2 ≤ m1+n1 → 𝐁❴m2,n2❵ ⊚ 𝐁❴m1,n1❵ ≘ 𝐁❴m1,n2+n1❵.
+#m2 elim m2 -m2
+[ #m1 #n2 #n1 #Hm21 #_
+  <(le_n_O_to_eq … Hm21) -m1 //
+| #m2 #IH *
+  [ #n2 #n1 #_ < plus_O_n #H
+    elim (le_inv_S1 … H) -H #x #Hx #H destruct
+    <plus_n_Sm
+    @after_push [4:|*: // ]
+    @(IH 0 … Hx) -IH -n2 -x //
+  | #m1 #n2 #n1 #H1 #H2
+    lapply (le_S_S_to_le … H1) -H1 #H1
+    lapply (le_S_S_to_le … H2) -H2 #H2
+    /3 width=7 by after_refl/
+  ]
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index 501d4f30f..bf3287912 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -25,14 +25,14 @@ table {
                "rtmap_fcla ( 𝐂⦃?⦄ ≘ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )"
                "rtmap_sle ( ? ⊆ ? )" "rtmap_sdj ( ? ∥ ? )" "rtmap_sand ( ? ⋒ ? ≘ ? )" "rtmap_sor ( ? ⋓ ? ≘ ? )"
                "rtmap_at ( @⦃?,?⦄ ≘ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≘ ? )" "rtmap_coafter ( ? ~⊚ ? ≘ ? )"
-               "rtmap_basic ( 𝐁❴?,?❵ )"
+               "rtmap_basic ( 𝐁❴?,?❵ )" "rtmap_basic_after"
              * ]
              [ "nstream ( ⫯? ) ( ↑? )" "nstream_eq" "" ""
                "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" ""
                "" "" "" ""
                "" "" "" "nstream_sor"
                "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
-               "nstream_basic"
+               "nstream_basic" ""
              * ]
 (*
              [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
diff --git a/matita/matita/contribs/lambdadelta/static_2/notation/relations/rlift_4.ma b/matita/matita/contribs/lambdadelta/static_2/notation/relations/rlift_4.ma
new file mode 100644
index 000000000..fb0fc24a7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/notation/relations/rlift_4.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⬆[ term 46 m, break term 46 n ] break term 46 T1 ≘ break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'RLift $m $n $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_basic.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_basic.ma
new file mode 100644
index 000000000..6d2ca03d9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_basic.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground_2/relocation/rtmap_basic_after.ma".
+include "static_2/notation/relations/rlift_4.ma".
+include "static_2/relocation/lifts.ma".
+
+(* GENERIC RELOCATION FOR TERMS *********************************************)
+
+interpretation "basic relocation (term)"
+   'RLift m n T1 T2 = (lifts (basic m n) T1 T2).
+
+(* Properties with basic relocation *****************************************)
+
+lemma lifts_lref_lt (m,n,i): i < m → ⬆[m,n] #i ≘ #i.
+/3 width=1 by lifts_lref, at_basic_lt/ qed.
+
+lemma lifts_lref_ge (m,n,i): m ≤ i → ⬆[m,n] #i ≘ #(n+i).
+/3 width=1 by lifts_lref, at_basic_ge/ qed.
+
+lemma lifts_lref_ge_minus (m,n,i): n+m ≤ i → ⬆[m,n] #(i-n) ≘ #i.
+#m #n #i #Hi
+>(plus_minus_m_m i n) in ⊢ (???%);
+/3 width=2 by lifts_lref_ge, le_plus_to_minus_l, le_plus_b/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma
index 828e2ad0f..358533f04 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma
@@ -92,6 +92,13 @@ lemma tdeq_inv_pair1: ∀h,o,I,V1,T1,Y. ②{I}V1.T1 ≛[h, o] Y →
                       ∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2.
 /2 width=3 by tdeq_inv_pair1_aux/ qed-.
 
+lemma tdeq_inv_sort2: ∀h,o,X1,s2. X1 ≛[h, o] ⋆s2 →
+                      ∃∃s1,d. deg h o s1 d & deg h o s2 d & X1 = ⋆s1.
+#h #o #X1 #s2 #H
+elim (tdeq_inv_sort1 h o X1 s2)
+/2 width=5 by tdeq_sym, ex3_2_intro/
+qed-.
+
 lemma tdeq_inv_pair2: ∀h,o,I,X1,V2,T2. X1 ≛[h, o] ②{I}V2.T2 →
                       ∃∃V1,T1. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & X1 = ②{I}V1.T1.
 #h #o #I #X1 #V2 #T2 #H
diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
index 4dcb17989..990057cc1 100644
--- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
@@ -75,11 +75,15 @@ table {
    ]
    class "orange"
    [ { "relocation" * } {
-        [ { "generic slicing" * } {
+        [ { "generic and uniform slicing" * } {
              [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_ctc" + "drops_ltc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_sex" + "drops_lex" + "drops_seq" + "drops_drops" + "drops_vector" * ]
           }
         ]
-        [ { "generic relocation" * } {
+        [ { "basic relocation" * } {
+             [ [ "for terms" ] "lifts_basic" + "( ⬆[?,?] ? ≘ ? )" * ]
+          }
+        ]
+        [ { "generic and uniform relocation" * } {
              [ [ "for binders" ] "lifts_bind" + "( ⬆*[?] ? ≘ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ]
              [ [ "for term vectors" ] "lifts_vector" + "( ⬆*[?] ? ≘ ? )" "lifts_lifts_vector" * ]
              [ [ "for terms" ] "lifts" + "( ⬆*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]