From bfd440cc2a790741616cae6b375609c6bbdc3b24 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 28 Oct 2019 20:37:33 +0100
Subject: [PATCH] update in basic_2
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

+ t-bound t-computarion for terms
+ validity rules in λδ-2A style justified
---
 .../lambdadelta/basic_2/dynamic/cnv_cpts.ma   |  74 ++++++
 .../basic_2/rt_computation/cpts.ma            | 153 +++++++++++++
 .../basic_2/rt_computation/cpts_aaa.ma        |  61 +++++
 .../basic_2/rt_computation/cpts_cpms.ma       |  35 +++
 .../basic_2/rt_computation/cpts_drops.ma      | 212 ++++++++++++++++++
 .../lambdadelta/basic_2/rt_transition/cpt.ma  |  75 ++++++-
 .../basic_2/rt_transition/cpt_drops.ma        | 111 ++++++++-
 .../lambdadelta/basic_2/web/basic_2.ldw.xml   |   4 +-
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |   6 +-
 9 files changed, 725 insertions(+), 6 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpts.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_aaa.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_cpms.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpts.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpts.ma
new file mode 100644
index 000000000..fc6d8e388
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpts.ma
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/cpts_cpms.ma".
+include "basic_2/rt_equivalence/cpcs_cpcs.ma".
+include "basic_2/rt_equivalence/cpes.ma".
+include "basic_2/dynamic/cnv_preserve_cpcs.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with t-bound t-computarion for terms **********************)
+
+lemma cpts_cpms_conf_eq (h) (n) (a) (G) (L):
+      ∀T0. ⦃G,L⦄ ⊢ T0 ![h,a] → ∀T1. ⦃G,L⦄ ⊢ T0 ⬆*[h,n] T1 →
+      ∀T2. ⦃G,L⦄ ⊢ T0 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2.
+#h #a #n #G #L #T0 #HT0 #T1 #HT01 #T2 #HT02
+/3 width=6 by cpts_fwd_cpms, cnv_cpms_conf_eq/
+qed-.
+
+(* Inversion lemmas with t-bound t-computarion for terms ********************)
+
+lemma cnv_inv_cast_cpts (h) (a) (nu) (nt) (G) (L):
+      ∀U1. ⦃G,L⦄ ⊢ U1 ![h,a] → ∀U2. ⦃G,L⦄ ⊢ U1 ⬆*[h,nu] U2 →
+      ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,nt] T2 →
+      ⦃G,L⦄ ⊢ U1 ⬌*[h,nu,nt] T1 → ⦃G,L⦄ ⊢ U2 ⬌*[h] T2.
+#h #a #nu #nt #G #L #U1 #HU1 #U2 #HU12 #T1 #HT1 #T2 #HT12 * #X1 #HUX1 #HTX1
+/3 width=8 by cpts_cpms_conf_eq, cpcs_canc_dx/
+qed-.
+
+lemma cnv_inv_appl_cpts (h) (a) (nv) (nt) (p) (G) (L):
+      ∀V1. ⦃G,L⦄ ⊢ V1 ![h,a] → ∀V2. ⦃G,L⦄ ⊢ V1 ⬆*[h,nv] V2 →
+      ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,nt] T2 →
+      ∀V0. ⦃G,L⦄ ⊢ V1 ➡*[nv,h] V0 → ∀T0. ⦃G,L⦄ ⊢ T1 ➡*[nt,h] ⓛ{p}V0.T0 →
+      ∃∃W0,U0. ⦃G,L⦄ ⊢ V2 ➡*[h] W0 & ⦃G,L⦄ ⊢ T2 ➡*[h] ⓛ{p}W0.U0.
+#h #a #nv #nt #p #G #L #V1 #HV1 #V2 #HV12 #T1 #HT1 #T2 #HT12 #V0 #HV20 #T0 #HT20
+lapply (cpts_cpms_conf_eq … HV1 … HV12 … HV20) -nv -V1 #HV20
+lapply (cpts_cpms_conf_eq … HT1 … HT12 … HT20) -nt -T1 #HT20
+lapply (cpcs_bind_sn … Abst … T0 HV20 p) -HV20 #HV20
+lapply (cpcs_canc_dx … HT20 … HV20) -V0 #HT20
+elim (cpcs_inv_cprs … HT20) -HT20 #X #HT2X #HT0X
+elim (cpms_inv_abst_sn … HT0X) -HT0X #V0 #X0 #HV20 #_ #H destruct
+/2 width=4 by ex2_2_intro/
+qed-.
+
+(* Properties with t-bound t-computarion for terms **************************)
+
+lemma cnv_cast_cpts (h) (a) (nu) (nt) (G) (L):
+      ∀U1. ⦃G,L⦄ ⊢ U1 ![h,a] → ∀U2. ⦃G,L⦄ ⊢ U1 ⬆*[h,nu] U2 →
+      ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,nt] T2 →
+      ⦃G,L⦄ ⊢ U2 ⬌*[h] T2 → ⦃G,L⦄ ⊢ U1 ⬌*[h,nu,nt] T1.
+#h #a #nu #nt #G #L #U1 #HU1 #U2 #HU12 #T1 #HT1 #T2 #HT12 #HUT2
+elim (cpcs_inv_cprs … HUT2) -HUT2 #X2 #HUX2 #HTX2
+/3 width=5 by cpts_cprs_trans, cpms_div/
+qed-.
+
+lemma cnv_appl_cpts (h) (a) (nv) (nt) (p) (G) (L):
+      ∀V1. ⦃G,L⦄ ⊢ V1 ![h,a] → ∀V2. ⦃G,L⦄ ⊢ V1 ⬆*[h,nv] V2 →
+      ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∀T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,nt] T2 →
+      ∀V0. ⦃G,L⦄ ⊢ V2 ➡*[h] V0 → ∀T0. ⦃G,L⦄ ⊢ T2 ➡*[h] ⓛ{p}V0.T0 →
+      ∃∃W0,U0. ⦃G,L⦄ ⊢ V1 ➡*[nv,h] W0 & ⦃G,L⦄ ⊢ T1 ➡*[nt,h] ⓛ{p}W0.U0.
+#h #a #nv #nt #p #G #L #V1 #HV1 #V2 #HV12 #T1 #HT1 #T2 #HT12 #V0 #HV20 #T0 #HT20
+/3 width=6 by cpts_cprs_trans, ex2_2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts.ma
new file mode 100644
index 000000000..24b6655b5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts.ma
@@ -0,0 +1,153 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lib/ltc.ma".
+include "basic_2/notation/relations/ptystar_6.ma".
+include "basic_2/rt_transition/cpt.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-COMPUTATION FOR TERMS ***************)
+
+definition cpts (h) (G) (L): relation3 nat term term ≝
+           ltc … plus … (cpt h G L).
+
+interpretation
+  "t-bound context-sensitive parallel t-computarion (term)"
+  'PTyStar h n G L T1 T2 = (cpts h G L n T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma cpts_ind_sn (h) (G) (L) (T2) (Q:relation2 …):
+                  Q 0 T2 →
+                  (∀n1,n2,T1,T. ⦃G,L⦄ ⊢ T1 ⬆[h,n1] T → ⦃G,L⦄ ⊢ T ⬆*[h,n2] T2 → Q n2 T → Q (n1+n2) T1) →
+                  ∀n,T1. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2 → Q n T1.
+#h #G #L #T2 #Q @ltc_ind_sn_refl //
+qed-.
+
+lemma cpts_ind_dx (h) (G) (L) (T1) (Q:relation2 …):
+                  Q 0 T1 →
+                  (∀n1,n2,T,T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,n1] T → Q n1 T → ⦃G,L⦄ ⊢ T ⬆[h,n2] T2 → Q (n1+n2) T2) →
+                  ∀n,T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2 → Q n T2.
+#h #G #L #T1 #Q @ltc_ind_dx_refl //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma cpt_cpts (h) (G) (L):
+      ∀n,T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2.
+/2 width=1 by ltc_rc/ qed.
+
+lemma cpts_step_sn (h) (G) (L):
+      ∀n1,T1,T. ⦃G,L⦄ ⊢ T1 ⬆[h,n1] T →
+      ∀n2,T2. ⦃G,L⦄ ⊢ T ⬆*[h,n2] T2 → ⦃G,L⦄ ⊢ T1 ⬆*[h,n1+n2] T2.
+/2 width=3 by ltc_sn/ qed-.
+
+lemma cpts_step_dx (h) (G) (L):
+      ∀n1,T1,T. ⦃G,L⦄ ⊢ T1 ⬆*[h,n1] T →
+      ∀n2,T2. ⦃G,L⦄ ⊢ T ⬆[h,n2] T2 → ⦃G,L⦄ ⊢ T1 ⬆*[h,n1+n2] T2.
+/2 width=3 by ltc_dx/ qed-.
+
+lemma cpts_bind_dx (h) (n) (G) (L):
+      ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 →
+      ∀I,T1,T2. ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆*[h,n] T2 →
+      ∀p. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆*[h,n] ⓑ{p,I}V2.T2.
+#h #n #G #L #V1 #V2 #HV12 #I #T1 #T2 #H #a @(cpts_ind_sn … H) -T1
+/3 width=3 by cpts_step_sn, cpt_cpts, cpt_bind/ qed.
+
+lemma cpts_appl_dx (h) (n) (G) (L):
+      ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 →
+      ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2 → ⦃G,L⦄ ⊢ ⓐV1.T1 ⬆*[h,n] ⓐV2.T2.
+#h #n #G #L #V1 #V2 #HV12 #T1 #T2 #H @(cpts_ind_sn … H) -T1
+/3 width=3 by cpts_step_sn, cpt_cpts, cpt_appl/
+qed.
+
+lemma cpts_ee (h) (n) (G) (L):
+      ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆*[h,n] U2 →
+      ∀T. ⦃G,L⦄ ⊢ ⓝU1.T ⬆*[h,↑n] U2.
+#h #n #G #L #U1 #U2 #H @(cpts_ind_sn … H) -U1 -n
+[ /3 width=1 by cpt_cpts, cpt_ee/
+| #n1 #n2 #U1 #U #HU1 #HU2 #_ #T >plus_S1
+  /3 width=3 by cpts_step_sn, cpt_ee/
+]
+qed.
+
+lemma cpts_refl (h) (G) (L): reflexive … (cpts h G L 0).
+/2 width=1 by cpt_cpts/ qed.
+
+(* Advanced properties ******************************************************)
+
+lemma cpts_sort (h) (G) (L) (n):
+      ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆*[h,n] ⋆((next h)^n s).
+#h #G #L #n elim n -n [ // ]
+#n #IH #s <plus_SO_dx
+/3 width=3 by cpts_step_dx, cpt_sort/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cpts_inv_sort_sn (h) (n) (G) (L) (s):
+      ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆*[h,n] X2 → X2 = ⋆(((next h)^n) s).
+#h #n #G #L #s #X2 #H @(cpts_ind_dx … H) -X2 //
+#n1 #n2 #X #X2 #_ #IH #HX2 destruct
+elim (cpt_inv_sort_sn … HX2) -HX2 #H #_ destruct //
+qed-.
+
+lemma cpts_inv_lref_sn_ctop (h) (n) (G) (i):
+      ∀X2. ⦃G,⋆⦄ ⊢ #i ⬆*[h,n] X2 → ∧∧ X2 = #i & n = 0.
+#h #n #G #i #X2 #H @(cpts_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+  elim (cpt_inv_lref_sn_ctop … HX2) -HX2 #H1 #H2 destruct
+  /2 width=1 by conj/
+]
+qed-.
+
+lemma cpts_inv_zero_sn_unit (h) (n) (I) (K) (G):
+      ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬆*[h,n] X2 → ∧∧ X2 = #0 & n = 0.
+#h #n #I #G #K #X2 #H @(cpts_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+  elim (cpt_inv_zero_sn_unit … HX2) -HX2 #H1 #H2 destruct
+  /2 width=1 by conj/
+]
+qed-.
+
+lemma cpts_inv_gref_sn (h) (n) (G) (L) (l):
+      ∀X2. ⦃G,L⦄ ⊢ §l ⬆*[h,n] X2 → ∧∧ X2 = §l & n = 0.
+#h #n #G #L #l #X2 #H @(cpts_ind_dx … H) -X2
+[ /2 width=1 by conj/
+| #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
+  elim (cpt_inv_gref_sn … HX2) -HX2 #H1 #H2 destruct
+  /2 width=1 by conj/
+]
+qed-.
+
+lemma cpts_inv_cast_sn (h) (n) (G) (L) (U1) (T1):
+      ∀X2. ⦃G,L⦄ ⊢ ⓝU1.T1 ⬆*[h,n] X2 →
+      ∨∨ ∃∃U2,T2. ⦃G,L⦄ ⊢ U1 ⬆*[h,n] U2 & ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2 & X2 = ⓝU2.T2
+       | ∃∃m. ⦃G,L⦄ ⊢ U1 ⬆*[h,m] X2 & n = ↑m.
+#h #n #G #L #U1 #T1 #X2 #H @(cpts_ind_dx … H) -n -X2
+[ /3 width=5 by or_introl, ex3_2_intro/
+| #n1 #n2 #X #X2 #_ * *
+  [ #U #T #HU1 #HT1 #H #HX2 destruct
+    elim (cpt_inv_cast_sn … HX2) -HX2 *
+    [ #U2 #T2 #HU2 #HT2 #H destruct
+      /4 width=5 by cpts_step_dx, ex3_2_intro, or_introl/
+    | #m #HX2 #H destruct <plus_n_Sm
+      /4 width=3 by cpts_step_dx, ex2_intro, or_intror/
+    ]
+  | #m #HX #H #HX2 destruct
+    /4 width=3 by cpts_step_dx, ex2_intro, or_intror/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_aaa.ma
new file mode 100644
index 000000000..a881796a5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_aaa.ma
@@ -0,0 +1,61 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/aaa.ma".
+include "basic_2/rt_computation/cpts_drops.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-COMPUTATION FOR TERMS ***************)
+
+(* Properties with atomic arity assignment for terms ************************)
+
+lemma cpts_total_aaa (h) (G) (L) (T1):
+      ∀A. ⦃G,L⦄ ⊢ T1 ⁝ A → ∀n. ∃T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2.
+#h #G #L #T1 #A #H elim H -G -L -T1 -A
+[ #G #L #s #n /3 width=2 by ex_intro/
+| #I #G #K #V1 #B #_ #IH #n -B
+  cases I -I
+  [ elim (IH n) -IH #V2 #HV12
+    elim (lifts_total V2 (𝐔❴1❵)) #T2 #HVT2
+    /3 width=4 by cpts_delta, ex_intro/
+  | cases n -n
+    [ /2 width=2 by ex_intro/
+    | #n elim (IH n) -IH #V2 #HV12
+      elim (lifts_total V2 (𝐔❴1❵)) #T2 #HVT2
+      /3 width=4 by cpts_ell, ex_intro/
+    ]
+  ]
+| #I #G #K #A #i #_ #IH #n -A
+  elim (IH n) -IH #T #HT
+  elim (lifts_total T (𝐔❴1❵)) #U #HTU
+  /3 width=4 by cpts_lref, ex_intro/
+| #p #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
+  elim (IHV 0) -IHV #V2 #HV12
+  elim (IHT n) -IHT #T2 #HT12
+  /3 width=3 by cpts_bind_dx, ex_intro/
+| #p #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
+  elim (IHV 0) -IHV #V2 #HV12
+  elim (IHT n) -IHT #T2 #HT12
+  /3 width=3 by cpts_bind_dx, ex_intro/
+| #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
+  elim (IHV 0) -IHV #V2 #HV12
+  elim (IHT n) -IHT #T2 #HT12
+  /3 width=3 by cpts_appl_dx, ex_intro/
+| #G #L #U1 #T1 #A #_ #_ #IHU #_ #n -A
+  cases n -n
+  [ /2 width=2 by ex_intro/
+  | #n elim (IHU n) -IHU #U2 #HU12
+    /3 width=3 by cpts_ee, ex_intro/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_cpms.ma
new file mode 100644
index 000000000..52e9bc8b8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_cpms.ma
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpt_cpm.ma".
+include "basic_2/rt_computation/cpms_cpms.ma".
+include "basic_2/rt_computation/cpts.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-COMPUTATION FOR TERMS ***************)
+
+(* Forward lemmas with t-bound rt-computation for terms *********************)
+
+lemma cpts_fwd_cpms (h) (n) (G) (L):
+      ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T2 → ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2.
+#h #n #G #L #T1 #T2 #H
+@(cpts_ind_dx … H) -n -T2 [ // ]
+#n1 #n2 #T #T2 #_ #IH #HT2
+/3 width=3 by cpms_step_dx, cpt_fwd_cpm/
+qed-.
+
+lemma cpts_cprs_trans (h) (n) (G) (L) (T):
+      ∀T1. ⦃G,L⦄ ⊢ T1 ⬆*[h,n] T →
+      ∀T2. ⦃G,L⦄ ⊢ T ➡*[h] T2 → ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2.
+#h #n #G #L #T #T1 #HT1 #T2 #HT2
+/3 width=3 by cpts_fwd_cpms, cpms_cprs_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma
new file mode 100644
index 000000000..66045be0e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_drops.ma
@@ -0,0 +1,212 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_ltc.ma".
+include "basic_2/rt_transition/cpt_drops.ma".
+include "basic_2/rt_computation/cpts.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-COMPUTATION FOR TERMS ***************)
+
+(* Properties with generic slicing for local environments *******************)
+
+lemma cpts_lifts_sn (h) (n) (G):
+      d_liftable2_sn … lifts (λL. cpts h G L n).
+/3 width=6 by d2_liftable_sn_ltc, cpt_lifts_sn/ qed-.
+
+lemma cpts_lifts_bi (h) (n) (G): 
+      d_liftable2_bi … lifts (λL. cpts h G L n).
+#h #n #G @d_liftable2_sn_bi
+/2 width=6 by cpts_lifts_sn, lifts_mono/
+qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+lemma cpts_inv_lifts_sn (h) (n) (G):
+      d_deliftable2_sn … lifts (λL. cpts h G L n).
+/3 width=6 by d2_deliftable_sn_ltc, cpt_inv_lifts_sn/ qed-.
+
+lemma cpts_inv_lifts_bi (h) (n) (G):
+      d_deliftable2_bi … lifts (λL. cpts h G L n).
+#h #n #G @d_deliftable2_sn_bi
+/2 width=6 by cpts_inv_lifts_sn, lifts_inj/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cpts_delta (h) (n) (G):
+      ∀K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆*[h,n] V2 →
+      ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓓV1⦄ ⊢ #0 ⬆*[h,n] W2.
+#h #n #G #K #V1 #V2 #H @(cpts_ind_dx … H) -V2
+[ /3 width=3 by cpt_cpts, cpt_delta/
+| #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2
+  elim (lifts_total V (𝐔❴1❵)) #W #HVW
+  /5 width=11 by cpts_step_dx, cpt_lifts_bi, drops_refl, drops_drop/
+]
+qed.
+
+lemma cpts_ell (h) (n) (G):
+      ∀K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆*[h,n] V2 →
+      ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓛV1⦄ ⊢ #0 ⬆*[h,↑n] W2.
+#h #n #G #K #V1 #V2 #H @(cpts_ind_dx … H) -V2
+[ /3 width=3 by cpt_cpts, cpt_ell/
+| #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2
+  elim (lifts_total V (𝐔❴1❵)) #W #HVW >plus_S1
+  /5 width=11 by cpts_step_dx, cpt_lifts_bi, drops_refl, drops_drop/
+]
+qed.
+
+lemma cpts_lref (h) (n) (I) (G):
+      ∀K,T,i. ⦃G,K⦄ ⊢ #i ⬆*[h,n] T →
+      ∀U. ⇧*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬆*[h,n] U.
+#h #n #I #G #K #T #i #H @(cpts_ind_dx … H) -T
+[ /3 width=3 by cpt_cpts, cpt_lref/
+| #n1 #n2 #T #T2 #_ #IH #HT2 #U2 #HTU2
+  elim (lifts_total T (𝐔❴1❵)) #U #TU
+  /5 width=11 by cpts_step_dx, cpt_lifts_bi, drops_refl, drops_drop/
+]
+qed.
+
+lemma cpts_cast_sn (h) (n) (G) (L):
+      ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆*[h,n] U2 →
+      ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ ⓝU1.T1 ⬆*[h,n] ⓝU2.T2.
+#h #n #G #L #U1 #U2 #H @(cpts_ind_sn … H) -U1 -n
+[ /3 width=3 by cpt_cpts, cpt_cast/
+| #n1 #n2 #U1 #U #HU1 #_ #IH #T1 #T2 #H
+  elim (cpt_fwd_plus … H) -H #T #HT1 #HT2
+  /3 width=3 by cpts_step_sn, cpt_cast/
+]
+qed.
+
+lemma cpts_delta_drops (h) (n) (G):
+      ∀L,K,V,i. ⇩*[i] L ≘ K.ⓓV →
+      ∀V2. ⦃G,K⦄ ⊢ V ⬆*[h,n] V2 →
+      ∀W2. ⇧*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬆*[h,n] W2.
+#h #n #G #L #K #V #i #HLK #V2 #H @(cpts_ind_dx … H) -V2
+[ /3 width=6 by cpt_cpts, cpt_delta_drops/
+| #n1 #n2 #V1 #V2 #_ #IH #HV12 #W2 #HVW2
+  lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK
+  elim (lifts_total V1 (𝐔❴↑i❵)) #W1 #HVW1
+  /3 width=11 by cpt_lifts_bi, cpts_step_dx/
+]
+qed.
+
+lemma cpts_ell_drops (h) (n) (G):
+      ∀L,K,W,i. ⇩*[i] L ≘ K.ⓛW →
+      ∀W2. ⦃G,K⦄ ⊢ W ⬆*[h,n] W2 →
+      ∀V2. ⇧*[↑i] W2 ≘ V2 → ⦃G,L⦄ ⊢ #i ⬆*[h,↑n] V2.
+#h #n #G #L #K #W #i #HLK #W2 #H @(cpts_ind_dx … H) -W2
+[ /3 width=6 by cpt_cpts, cpt_ell_drops/
+| #n1 #n2 #W1 #W2 #_ #IH #HW12 #V2 #HWV2
+  lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK
+  elim (lifts_total W1 (𝐔❴↑i❵)) #V1 #HWV1 >plus_S1
+  /3 width=11 by cpt_lifts_bi, cpts_step_dx/
+]
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpts_inv_lref_sn_drops (h) (n) (G) (L) (i):
+      ∀X2. ⦃G,L⦄ ⊢ #i ⬆*[h,n] X2 →
+      ∨∨ ∧∧ X2 = #i & n = 0
+       | ∃∃K,V,V2. ⇩*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V ⬆*[h,n] V2 & ⇧*[↑i] V2 ≘ X2
+       | ∃∃m,K,V,V2. ⇩*[i] L ≘ K.ⓛV & ⦃G,K⦄ ⊢ V ⬆*[h,m] V2 & ⇧*[↑i] V2 ≘ X2 & n = ↑m.
+#h #n #G #L #i #X2 #H @(cpts_ind_dx … H) -X2
+[ /3 width=1 by or3_intro0, conj/
+| #n1 #n2 #T #T2 #_ #IH #HT2 cases IH -IH *
+  [ #H1 #H2 destruct
+    elim (cpt_inv_lref_sn_drops … HT2) -HT2 *
+    [ /3 width=1 by or3_intro0, conj/
+    | /4 width=6 by cpt_cpts, or3_intro1, ex3_3_intro/
+    | /4 width=8 by cpt_cpts, or3_intro2, ex4_4_intro/
+    ]
+  | #K #V0 #V #HLK #HV0 #HVT
+    lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
+    elim (cpt_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T
+    /4 width=6 by cpts_step_dx, ex3_3_intro, or3_intro1/
+  | #m #K #V0 #V #HLK #HV0 #HVT #H destruct
+    lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
+    elim (cpt_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T
+    /4 width=8 by cpts_step_dx, ex4_4_intro, or3_intro2/
+  ]
+]
+qed-.
+
+lemma cpts_inv_delta_sn (h) (n) (G) (K) (V):
+      ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 ⬆*[h,n] X2 →
+      ∨∨ ∧∧ X2 = #0 & n = 0
+       | ∃∃V2. ⦃G,K⦄ ⊢ V ⬆*[h,n] V2 & ⇧*[1] V2 ≘ X2.
+#h #n #G #K #V #X2 #H
+elim (cpts_inv_lref_sn_drops … H) -H *
+[ /3 width=1 by or_introl, conj/
+| #Y #X #V2 #H #HV2 #HVT2
+  lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+  /3 width=3 by ex2_intro, or_intror/
+| #m #Y #X #V2 #H #HV2 #HVT2
+  lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+]
+qed-.
+
+lemma cpts_inv_ell_sn (h) (n) (G) (K) (V):
+      ∀X2. ⦃G,K.ⓛV⦄ ⊢ #0 ⬆*[h,n] X2 →
+      ∨∨ ∧∧ X2 = #0 & n = 0
+       | ∃∃m,V2. ⦃G,K⦄ ⊢ V ⬆*[h,m] V2 & ⇧*[1] V2 ≘ X2 & n = ↑m.
+#h #n #G #K #V #X2 #H
+elim (cpts_inv_lref_sn_drops … H) -H *
+[ /3 width=1 by or_introl, conj/
+| #Y #X #V2 #H #HV2 #HVT2
+  lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+| #m #Y #X #V2 #H #HV2 #HVT2 #H0 destruct
+  lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+  /3 width=5 by ex3_2_intro, or_intror/
+]
+qed-.
+
+lemma cpts_inv_lref_sn (h) (n) (I) (G) (K) (i):
+      ∀X2. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬆*[h,n] X2 →
+      ∨∨ ∧∧ X2 = #↑i & n = 0
+       | ∃∃T2. ⦃G,K⦄ ⊢ #i ⬆*[h,n] T2 & ⇧*[1] T2 ≘ X2.
+#h #n #I #G #K #i #X2 #H
+elim (cpts_inv_lref_sn_drops … H) -H *
+[ /3 width=1 by or_introl, conj/
+| #L #V #V2 #H #HV2 #HVU2
+  lapply (drops_inv_drop1 … H) -H #HLK
+  elim (lifts_split_trans … HVU2 (𝐔❴↑i❵) (𝐔❴1❵)) -HVU2
+  [| // ] #T2 #HVT2 #HTU2
+  /4 width=6 by cpts_delta_drops, ex2_intro, or_intror/
+| #m #L #V #V2 #H #HV2 #HVU2 #H0 destruct
+  lapply (drops_inv_drop1 … H) -H #HLK
+  elim (lifts_split_trans … HVU2 (𝐔❴↑i❵) (𝐔❴1❵)) -HVU2
+  [| // ] #T2 #HVT2 #HTU2
+  /4 width=6 by cpts_ell_drops, ex2_intro, or_intror/
+]
+qed-.
+
+lemma cpts_inv_succ_sn (h) (n) (G) (L):
+      ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆*[h,↑n] T2 →
+      ∃∃T. ⦃G,L⦄ ⊢ T1 ⬆*[h,1] T & ⦃G,L⦄ ⊢ T ⬆*[h,n] T2.
+#h #n #G #L #T1 #T2
+@(insert_eq_0 … (↑n)) #m #H
+@(cpts_ind_sn … H) -T1 -m
+[ #H destruct
+| #x1 #n2 #T1 #T #HT1 #HT2 #IH #H
+  elim (plus_inv_S3_sn x1 n2) [1,2: * |*: // ] -H
+  [ #H1 #H2 destruct -HT2
+    elim IH -IH // #T0 #HT0 #HT02
+    /3 width=3 by cpts_step_sn, ex2_intro/
+  | #n1 #H1 #H2 destruct -IH
+    elim (cpt_fwd_plus … 1 n1 … T1 T) [|*: // ] -HT1 #T0 #HT10 #HT0
+    /3 width=5 by cpts_step_sn, cpt_cpts, ex2_intro/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma
index 229c32a96..53f9d778d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma
@@ -81,11 +81,17 @@ lemma cpt_ee (h) (n) (G) (L):
 /3 width=3 by cpg_ee, ist_succ, ex2_intro/
 qed.
 
-(* Basic properties *********************************************************)
-
 lemma cpt_refl (h) (G) (L): reflexive … (cpt h G L 0).
 /3 width=3 by cpg_refl, ex2_intro/ qed.
 
+(* Advanced properties ******************************************************)
+
+lemma cpt_sort (h) (G) (L):
+      ∀n. n ≤ 1 → ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] ⋆((next h)^n s).
+#h #G #L * //
+#n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/
+qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma cpt_inv_atom_sn (h) (n) (J) (G) (L):
@@ -109,6 +115,71 @@ elim (cpg_inv_atom1 … H) -H *
 ]
 qed-.
 
+lemma cpt_inv_sort_sn (h) (n) (G) (L) (s):
+      ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] X2 →
+      ∧∧ X2 = ⋆(((next h)^n) s) & n ≤ 1.
+#h #n #G #L #s #X2 * #c #Hc #H
+elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct
+/2 width=1 by conj/
+qed-.
+
+lemma cpt_inv_zero_sn (h) (n) (G) (L):
+      ∀X2. ⦃G,L⦄ ⊢ #0 ⬆[h,n] X2 →
+      ∨∨ ∧∧ X2 = #0 & n = 0
+       | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1
+       | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & n = ↑m.
+#h #n #G #L #X2 * #c #Hc #H elim (cpg_inv_zero1 … H) -H *
+[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or3_intro0, conj/
+| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
+  /4 width=8 by or3_intro1, ex3_3_intro, ex2_intro/
+| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
+  elim (ist_inv_plus_SO_dx … H2) -H2 // #m #Hc #H destruct
+  /4 width=8 by or3_intro2, ex4_4_intro, ex2_intro/
+]
+qed-.
+
+lemma cpt_inv_zero_sn_unit (h) (n) (I) (K) (G):
+      ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬆[h,n] X2 → ∧∧ X2 = #0 & n = 0.
+#h #n #I #G #K #X2 #H
+elim (cpt_inv_zero_sn … H) -H *
+[ #H1 #H2 destruct /2 width=1 by conj/
+| #Y #X1 #X2 #_ #_ #H destruct
+| #m #Y #X1 #X2 #_ #_ #H destruct
+]
+qed.
+
+lemma cpt_inv_lref_sn (h) (n) (G) (L) (i):
+      ∀X2. ⦃G,L⦄ ⊢ #↑i ⬆[h,n] X2 →
+      ∨∨ ∧∧ X2 = #(↑i) & n = 0
+       | ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I}.
+#h #n #G #L #i #X2 * #c #Hc #H elim (cpg_inv_lref1 … H) -H *
+[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or_introl, conj/
+| #I #K #V2 #HV2 #HVT2 #H destruct
+ /4 width=6 by ex3_3_intro, ex2_intro, or_intror/
+]
+qed-.
+
+lemma cpt_inv_lref_sn_ctop (n) (h) (G) (i):
+      ∀X2. ⦃G,⋆⦄ ⊢ #i ⬆[h,n] X2 → ∧∧ X2 = #i & n = 0.
+#h #n #G * [| #i ] #X2 #H
+[ elim (cpt_inv_zero_sn … H) -H *
+  [ #H1 #H2 destruct /2 width=1 by conj/
+  | #Y #X1 #X2 #_ #_ #H destruct
+  | #m #Y #X1 #X2 #_ #_ #H destruct
+  ]
+| elim (cpt_inv_lref_sn … H) -H *
+  [ #H1 #H2 destruct /2 width=1 by conj/
+  | #Z #Y #X0 #_ #_ #H destruct
+  ]
+]
+qed.
+
+lemma cpt_inv_gref_sn (h) (n) (G) (L) (l):
+      ∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0.
+#h #n #G #L #l #X2 * #c #Hc #H elim (cpg_inv_gref1 … H) -H
+#H1 #H2 destruct /2 width=1 by conj/ 
+qed-.
+
 lemma cpt_inv_bind_sn (h) (n) (p) (I) (G) (L) (V1) (T1):
       ∀X2. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] X2 →
       ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma
index 6447e51ae..707ecb19d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/rt_transition/cpg_drops.ma".
-include "basic_2/rt_transition/cpt.ma".
+include "basic_2/rt_transition/cpt_fqu.ma".
 
 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
 
@@ -44,3 +44,112 @@ lemma cpt_inv_lifts_bi (h) (n) (G):
       d_deliftable2_bi … lifts (λL. cpt h G L n).
 #h #n #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/
 qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cpt_delta_drops (h) (n) (G):
+      ∀L,K,V,i. ⇩*[i] L ≘ K.ⓓV → ∀V2. ⦃G,K⦄ ⊢ V ⬆[h,n] V2 →
+      ∀W2. ⇧*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬆[h,n] W2.
+#h #n #G #L #K #V #i #HLK #V2 *
+/3 width=8 by cpg_delta_drops, ex2_intro/
+qed.
+
+lemma cpt_ell_drops (h) (n) (G):
+      ∀L,K,V,i. ⇩*[i] L ≘ K.ⓛV → ∀V2. ⦃G,K⦄ ⊢ V ⬆[h,n] V2 →
+      ∀W2. ⇧*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬆[h,↑n] W2.
+#h #n #G #L #K #V #i #HLK #V2 *
+/3 width=8 by cpg_ell_drops, ist_succ, ex2_intro/
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpt_inv_atom_sn_drops (h) (n) (I) (G) (L):
+      ∀X2. ⦃G,L⦄ ⊢ ⓪{I} ⬆[h,n] X2 →
+      ∨∨ ∧∧ X2 = ⓪{I} & n = 0
+       | ∃∃s. X2 = ⋆(⫯[h]s) & I = Sort s & n = 1
+       | ∃∃K,V,V2,i. ⇩*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V ⬆[h,n] V2 & ⇧*[↑i] V2 ≘ X2 & I = LRef i
+       | ∃∃m,K,V,V2,i. ⇩*[i] L ≘ K.ⓛV & ⦃G,K⦄ ⊢ V ⬆[h,m] V2 & ⇧*[↑i] V2 ≘ X2 & I = LRef i & n = ↑m.
+#h #n #I #G #L #X2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
+[ #H1 #H2 destruct
+  /3 width=1 by or4_intro0, conj/
+| #s #H1 #H2 #H3 destruct
+  /3 width=3 by or4_intro1, ex3_intro/
+| #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
+  /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/
+| #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
+  elim (ist_inv_plus_SO_dx … H2) -H2
+  /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/
+]
+qed-.
+
+lemma cpt_inv_lref_sn_drops (h) (n) (G) (L) (i):
+      ∀X2. ⦃G,L⦄ ⊢ #i ⬆[h,n] X2 →
+      ∨∨ ∧∧ X2 = #i & n = 0
+       | ∃∃K,V,V2. ⇩*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V ⬆[h,n] V2 & ⇧*[↑i] V2 ≘ X2
+       | ∃∃m,K,V,V2. ⇩*[i] L ≘ K. ⓛV & ⦃G,K⦄ ⊢ V ⬆[h,m] V2 & ⇧*[↑i] V2 ≘ X2 & n = ↑m.
+#h #n #G #L #i #X2 * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H *
+[ #H1 #H2 destruct
+  /3 width=1 by or3_intro0, conj/
+| #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
+  /4 width=6 by ex3_3_intro, ex2_intro, or3_intro1/
+| #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
+  elim (ist_inv_plus_SO_dx … H) -H
+  /4 width=8 by ex4_4_intro, ex2_intro, or3_intro2/
+]
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+fact cpt_fwd_plus_aux (h) (n) (G) (L):
+     ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ∀n1,n2. n1+n2 = n →
+     ∃∃T. ⦃G,L⦄ ⊢ T1 ⬆[h,n1] T & ⦃G,L⦄ ⊢ T ⬆[h,n2] T2.
+#h #n #G #L #T1 #T2 #H @(cpt_ind … H) -G -L -T1 -T2 -n
+[ #I #G #L #n1 #n2 #H
+  elim (plus_inv_O3 … H) -H #H1 #H2 destruct
+  /2 width=3 by ex2_intro/
+| #G #L #s #x1 #n2 #H
+  elim (plus_inv_S3_sn … H) -H *
+  [ #H1 #H2 destruct /2 width=3 by ex2_intro/
+  | #n1 #H1 #H elim (plus_inv_O3 … H) -H #H2 #H3 destruct
+    /2 width=3 by ex2_intro/
+  ]
+| #n #G #K #V1 #V2 #W2 #_ #IH #HVW2 #n1 #n2 #H destruct
+  elim IH [|*: // ] -IH #V #HV1 #HV2
+  elim (lifts_total V 𝐔❴↑O❵) #W #HVW
+  /5 width=11 by cpt_lifts_bi, cpt_delta, drops_refl, drops_drop, ex2_intro/
+| #n #G #K #V1 #V2 #W2 #HV12 #IH #HVW2 #x1 #n2 #H
+  elim (plus_inv_S3_sn … H) -H *
+  [ #H1 #H2 destruct -IH /3 width=3 by cpt_ell, ex2_intro/
+  | #n1 #H1 #H2 destruct -HV12
+    elim (IH n1) [|*: // ] -IH #V #HV1 #HV2
+    elim (lifts_total V 𝐔❴↑O❵) #W #HVW
+    /5 width=11 by cpt_lifts_bi, cpt_ell, drops_refl, drops_drop, ex2_intro/
+  ]
+| #n #I #G #K #T2 #U2 #i #_ #IH #HTU2 #n1 #n2 #H destruct
+  elim IH [|*: // ] -IH #T #HT1 #HT2
+  elim (lifts_total T 𝐔❴↑O❵) #U #HTU
+  /5 width=11 by cpt_lifts_bi, cpt_lref, drops_refl, drops_drop, ex2_intro/
+| #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
+  elim IHT [|*: // ] -IHT #T #HT1 #HT2
+  /3 width=5 by cpt_bind, ex2_intro/
+| #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
+  elim IHT [|*: // ] -IHT #T #HT1 #HT2
+  /3 width=5 by cpt_appl, ex2_intro/
+| #n #G #L #U1 #U2 #T1 #T2 #_ #_ #IHU #IHT #n1 #n2 #H destruct
+  elim IHU [|*: // ] -IHU #U #HU1 #HU2
+  elim IHT [|*: // ] -IHT #T #HT1 #HT2
+  /3 width=5 by cpt_cast, ex2_intro/
+| #n #G #L #U1 #U2 #T #HU12 #IH #x1 #n2 #H
+  elim (plus_inv_S3_sn … H) -H *
+  [ #H1 #H2 destruct -IH /3 width=4 by cpt_ee, cpt_cast, ex2_intro/
+  | #n1 #H1 #H2 destruct -HU12
+    elim (IH n1) [|*: // ] -IH #U #HU1 #HU2
+    /3 width=3 by cpt_ee, ex2_intro/
+  ]
+]
+qed-.
+
+lemma cpt_fwd_plus (h) (n1) (n2) (G) (L):
+      ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n1+n2] T2 →
+      ∃∃T. ⦃G,L⦄ ⊢ T1 ⬆[h,n1] T & ⦃G,L⦄ ⊢ T ⬆[h,n2] T2.
+/2 width=3 by cpt_fwd_plus_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
index 1be3304c9..28575ff0e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -46,7 +46,7 @@
          (i.e. no induction on the degree).
    </news>
    <news class="beta" date="2018 November 1.">
-         Extended (λδ-2A) and restricted (λδ-1A) type rules justified.
+         Extended (λδ-2A) and restricted (λδ-1B) validity rules justified.
    </news>
    <news class="alpha" date="2018 September 21.">
          λδ-2A completed with
@@ -102,7 +102,7 @@
          λδ-2A appears too complex and is dismissed.
    </news>
    <news class="gamma" date="2014 October 28.">
-         λδ version 2A is released.
+         λδ-2A is released.
    </news>
    <news class="beta" date="2014 September 9.">
          Iterated static type assignment defined (more elegantly)
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 6bf92c3c1..6e4575ba0 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
@@ -25,7 +25,7 @@ table {
         ]
         [ { "context-sensitive native validity" * } {
              [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
-             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_cpts" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" + "cnv_eval" * ]
           }
         ]
      }
@@ -60,6 +60,10 @@ table {
    ]
    class "sky"
    [ { "rt-computation" * } {
+        [ { "context-sensitive parallel t-computation" * } {
+             [ [ "for terms" ] "cpts" + "( ⦃?,?⦄ ⊢ ? ⬆*[?,?] ? )" "cpts_drops" + "cpts_aaa" + "cpts_cpms" * ]
+          }
+        ]
         [ { "context-sensitive parallel r-computation" * } {
              [ [ "evaluation for terms" ] "cpre ( ⦃?,?⦄ ⊢ ? ➡*[?] 𝐍⦃?⦄ )" "cpre_csx" + "cpre_cpms" + "cpre_cpre" * ]
              [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ]
-- 
2.39.2