From 6f06bee3eeb4f718b273f0cca5873e9dc5e758b2 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 13 Sep 2016 19:23:02 +0000
Subject: [PATCH] more results on cpm ...

---
 .../lambdadelta/basic_2/etc_new/cpr/cpr.etc   |  29 +++++
 .../{rt_transition => etc_new/cpr}/cpr_cir.ma |   0
 .../basic_2/rt_transition/cpm_cpx.ma          |  26 ++++
 .../basic_2/rt_transition/cpm_drops.ma        |  95 +++++++++++++++
 .../basic_2/rt_transition/cpm_lsubr.ma        |  33 ++++++
 .../basic_2/rt_transition/cpm_simple.ma       |  30 +++++
 .../lambdadelta/basic_2/rt_transition/cpr.etc |  87 --------------
 .../basic_2/rt_transition/cpr_drops.ma        |  45 +++++++
 .../basic_2/rt_transition/cpr_lift.ma         | 112 ------------------
 .../basic_2/rt_transition/cpx_drops.ma        |   2 +-
 .../basic_2/rt_transition/cpx_lsubr.ma        |   2 +
 .../basic_2/rt_transition/partial.txt         |   4 +-
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |   9 +-
 13 files changed, 268 insertions(+), 206 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr.etc
 rename matita/matita/contribs/lambdadelta/basic_2/{rt_transition => etc_new/cpr}/cpr_cir.ma (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_simple.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr.etc
new file mode 100644
index 000000000..3f30e621f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr.etc
@@ -0,0 +1,29 @@
+lemma cpr_delift: ∀G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓓV) →
+                  ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡ T2 & ⬆[l, 1] T ≡ T2.
+#G #K #V #T1 elim T1 -T1
+[ * /2 width=4 by cpr_atom, lift_sort, lift_gref, ex2_2_intro/
+  #i #L #l #HLK elim (lt_or_eq_or_gt i l)
+  #Hil [1,3: /4 width=4 by lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ]
+  destruct
+  elim (lift_total V 0 (i+1)) #W #HVW
+  elim (lift_split … HVW i i) /3 width=6 by cpr_delta, ex2_2_intro/
+| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #l #HLK
+  elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
+  [ elim (IHU1 (L. ⓑ{I}W1) (l+1)) -IHU1 /3 width=9 by drop_drop, cpr_bind, lift_bind, ex2_2_intro/
+  | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpr_flat, lift_flat, ex2_2_intro/
+  ]
+]
+qed-.
+
+fact lstas_cpr_aux: ∀h,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*[h, d] T2 →
+                    d = 0 → ⦃G, L⦄ ⊢ T1 ➡ T2.
+#h #G #L #T1 #T2 #d #H elim H -G -L -T1 -T2 -d
+/3 width=1 by cpr_eps, cpr_flat, cpr_bind/
+[ #G #L #K #V1 #V2 #W2 #i #d #HLK #_ #HVW2 #IHV12 #H destruct
+  /3 width=6 by cpr_delta/
+| #G #L #K #V1 #V2 #W2 #i #d #_ #_ #_ #_ <plus_n_Sm #H destruct
+]
+qed-.
+
+lemma lstas_cpr: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, 0] T2 → ⦃G, L⦄ ⊢ T1 ➡ T2.
+/2 width=4 by lstas_cpr_aux/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr_cir.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_cir.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr_cir.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma
new file mode 100644
index 000000000..d459fff2a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpx.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Forward lemmas with uncounted context-sensitive rt-transition for terms **)
+
+(* Basic_2A1: includes: cpr_cpx *)
+lemma cpm_fwd_cpx: ∀n,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2.
+#n #h #G #L #T1 #T2 * #c #Hc #H elim H -L -T1 -T2
+/2 width=3 by cpx_theta, cpx_beta, cpx_ee, cpx_eps, cpx_zeta, cpx_flat, cpx_bind, cpx_lref, cpx_delta/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma
new file mode 100644
index 000000000..786d2f9ce
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma
@@ -0,0 +1,95 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpg_drops.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: includes: pr2_delta1 *)
+(* Basic_2A1: includes: cpr_delta *)
+lemma cpm_delta_drops: ∀n,h,G,L,K,V,V2,W2,i.
+                       ⬇*[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡[n, h] V2 →
+                       ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡[n, h] W2.
+#n #h #G #L #K #V #V2 #W2 #i #HLK *
+/3 width=8 by cpg_delta_drops, ex2_intro/
+qed.
+
+lemma cpm_ell_drops: ∀n,h,G,L,K,V,V2,W2,i.
+                     ⬇*[i] L ≡ K.ⓛV → ⦃G, K⦄ ⊢ V ➡[n, h] V2 →
+                     ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡[⫯n, h] W2.
+#n #h #G #L #K #V #V2 #W2 #i #HLK *
+/3 width=8 by cpg_ell_drops, isrt_succ, ex2_intro/
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpm_inv_atom1_drops: ∀n,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[n, h] T2 →
+                           ∨∨ T2 = ⓪{I} ∧ n = 0
+                            | ∃∃s. T2 = ⋆(next h s) & I = Sort s & n = 1
+                            | ∃∃K,V,V2,i. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 &
+                                          ⬆*[⫯i] V2 ≡ T2 & I = LRef i
+                            | ∃∃m,K,V,V2,i. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ➡[m, h] V2 &
+                                            ⬆*[⫯i] V2 ≡ T2 & I = LRef i & n = ⫯m.
+#n #h #I #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
+[ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
+  /3 width=1 by or4_intro0, conj/
+| #s #H1 #H2 #H3 destruct lapply (isrt_inv_01 … Hc) -Hc
+  /4 width=3 by or4_intro1, ex3_intro, sym_eq/ (**) (* sym_eq *)
+| #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 (isrt_inv_plus_SO_dx … Hc) -Hc
+  /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/
+]
+qed-.
+
+lemma cpm_inv_lref1_drops: ∀n,h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[n, h] T2 →
+                           ∨∨ T2 = #i ∧ n = 0
+                            | ∃∃K,V,V2. ⬇*[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 &
+                                        ⬆*[⫯i] V2 ≡ T2
+                            | ∃∃m,K,V,V2. ⬇*[i] L ≡ K. ⓛV & ⦃G, K⦄ ⊢ V ➡[m, h] V2 &
+                                          ⬆*[⫯i] V2 ≡ T2 & n = ⫯m.
+#n #h #G #L #T2 #i * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H *
+[ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
+  /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 (isrt_inv_plus_SO_dx … Hc) -Hc
+  /4 width=8 by ex4_4_intro, ex2_intro, or3_intro2/
+]
+qed-.
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_1: includes: pr0_lift pr2_lift *)
+(* Basic_2A1: includes: cpr_lift *)
+lemma cpm_lifts: ∀n,h,G. d_liftable2 (cpm n h G).
+#n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
+elim (cpg_lifts … HT12 … HLK … HTU1) -K -T1
+/3 width=5 by ex2_intro/
+qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
+(* Basic_2A1: includes: cpr_inv_lift1 *)
+lemma cpm_inv_lifts1: ∀n,h,G. d_deliftable2_sn (cpm n h G).
+#n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
+elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1
+/3 width=5 by ex2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma
new file mode 100644
index 000000000..ac03ed30c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.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 "basic_2/rt_transition/cpg_lsubr.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Properties with restricted refinement for local environments *************)
+
+(* Basic_2A1: includes: lsubr_cpr_trans *)
+lemma lsubr_cpm_trans: ∀n,h,G. lsub_trans … (cpm n h G) lsubr.
+#n #h #G #L1 #T1 #T2 * /3 width=5 by lsubr_cpg_trans, ex2_intro/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was by definition: pr2_free *)
+(* Basic_2A1: includes: tpr_cpr *)
+lemma tpm_cpm: ∀n,h,G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡[n, h] T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2.
+#n #h #G #T1 #T2 #HT12 #L lapply (lsubr_cpm_trans … HT12 L ?) //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_simple.ma
new file mode 100644
index 000000000..9a37802e6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_simple.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/rt_transition/cpg_simple.ma".
+include "basic_2/rt_transition/cpm.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+
+(* Properties with simple terms *********************************************)
+
+(* Basic_2A1: includes: cpr_inv_appl1_simple *)
+lemma cpm_inv_appl1_simple: ∀n,h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡[n, h] U → 𝐒⦃T1⦄ →
+                            ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 &
+                                     U = ⓐV2.T2.
+#n #h #G #L #V1 #T1 #U * #c #Hc #H #HT1 elim (cpg_inv_appl1_simple … H HT1) -H -HT1
+#cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct elim (isrt_inv_max … Hc) -Hc
+#nV #nT #HnV #HnT #H destruct elim (isrt_inv_shift … HnV) -HnV
+#HnV #H destruct /3 width=5 by ex3_2_intro, ex2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.etc b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.etc
deleted file mode 100644
index dee79d193..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.etc
+++ /dev/null
@@ -1,87 +0,0 @@
-(* Basic_1: includes: pr2_delta1 *)
-| cpr_delta: ∀G,L,K,V,V2,W2,i.
-             ⬇[i] L ≡ K. ⓓV → cpr G K V V2 →
-             ⬆[0, i + 1] V2 ≡ W2 → cpr G L (#i) W2
-
-lemma cpr_cpx: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2.
-#h #o #G #L #T1 #T2 #H elim H -L -T1 -T2
-/2 width=7 by cpx_delta, cpx_bind, cpx_flat, cpx_zeta, cpx_eps, cpx_beta, cpx_theta/
-qed.
-
-lemma lsubr_cpr_trans: ∀G. lsub_trans … (cpr G) lsubr.
-#G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
-[ //
-| #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (lsubr_fwd_drop2_abbr … HL12 … HLK1) -L1 *
-  /3 width=6 by cpr_delta/
-|3,7: /4 width=1 by lsubr_pair, cpr_bind, cpr_beta/
-|4,6: /3 width=1 by cpr_flat, cpr_eps/
-|5,8: /4 width=3 by lsubr_pair, cpr_zeta, cpr_theta/
-]
-qed-.
-
-(* Basic_1: was by definition: pr2_free *)
-lemma tpr_cpr: ∀G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡ T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡ T2.
-#G #T1 #T2 #HT12 #L
-lapply (lsubr_cpr_trans … HT12 L ?) //
-qed.
-
-lemma cpr_delift: ∀G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓓV) →
-                  ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡ T2 & ⬆[l, 1] T ≡ T2.
-#G #K #V #T1 elim T1 -T1
-[ * /2 width=4 by cpr_atom, lift_sort, lift_gref, ex2_2_intro/
-  #i #L #l #HLK elim (lt_or_eq_or_gt i l)
-  #Hil [1,3: /4 width=4 by lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ]
-  destruct
-  elim (lift_total V 0 (i+1)) #W #HVW
-  elim (lift_split … HVW i i) /3 width=6 by cpr_delta, ex2_2_intro/
-| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #l #HLK
-  elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
-  [ elim (IHU1 (L. ⓑ{I}W1) (l+1)) -IHU1 /3 width=9 by drop_drop, cpr_bind, lift_bind, ex2_2_intro/
-  | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpr_flat, lift_flat, ex2_2_intro/
-  ]
-]
-qed-.
-
-fact lstas_cpr_aux: ∀h,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*[h, d] T2 →
-                    d = 0 → ⦃G, L⦄ ⊢ T1 ➡ T2.
-#h #G #L #T1 #T2 #d #H elim H -G -L -T1 -T2 -d
-/3 width=1 by cpr_eps, cpr_flat, cpr_bind/
-[ #G #L #K #V1 #V2 #W2 #i #d #HLK #_ #HVW2 #IHV12 #H destruct
-  /3 width=6 by cpr_delta/
-| #G #L #K #V1 #V2 #W2 #i #d #_ #_ #_ #_ <plus_n_Sm #H destruct
-]
-qed-.
-
-lemma lstas_cpr: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, 0] T2 → ⦃G, L⦄ ⊢ T1 ➡ T2.
-/2 width=4 by lstas_cpr_aux/ qed.
-
-lemma cpr_inv_atom1: ∀I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡ T2 →
-                     T2 = ⓪{I} ∨
-                     ∃∃K,V,V2,i. ⬇[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
-                                 ⬆[O, i + 1] V2 ≡ T2 & I = LRef i.
-/2 width=3 by cpr_inv_atom1_aux/ qed-.
-
-(* Basic_1: includes: pr0_gen_lref pr2_gen_lref *)
-lemma cpr_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡ T2 →
-                     T2 = #i ∨
-                     ∃∃K,V,V2. ⬇[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
-                               ⬆[O, i + 1] V2 ≡ T2.
-#G #L #T2 #i #H
-elim (cpr_inv_atom1 … H) -H /2 width=1 by or_introl/
-* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6 by ex3_3_intro, or_intror/
-qed-.
-
-(* Note: the main property of simple terms *)
-lemma cpr_inv_appl1_simple: ∀G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
-                            ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ T1 ➡ T2 &
-                                     U = ⓐV2. T2.
-#G #L #V1 #T1 #U #H #HT1
-elim (cpr_inv_appl1 … H) -H *
-[ /2 width=5 by ex3_2_intro/
-| #a #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H #_ destruct
-  elim (simple_inv_bind … HT1)
-| #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
-  elim (simple_inv_bind … HT1)
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma
new file mode 100644
index 000000000..48d281e4f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma
@@ -0,0 +1,45 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpm_drops.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_2A1: includes: cpr_inv_atom1 *)
+lemma cpr_inv_atom1_drops: ∀h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[h] T2 →
+                           T2 = ⓪{I} ∨
+                           ∃∃K,V,V2,i. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 &
+                                       ⬆*[⫯i] V2 ≡ T2 & I = LRef i.
+#h #I #G #L #T2 #H elim (cpm_inv_atom1_drops … H) -H *
+[ /2 width=1 by or_introl/
+| #s #_ #_ #H destruct
+| /3 width=8 by ex4_4_intro, or_intror/
+| #m #K #V1 #V2 #i #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_1: includes: pr0_gen_lref pr2_gen_lref *)
+(* Basic_2A1: includes: cpr_inv_lref1 *)
+lemma cpr_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h] T2 →
+                           T2 = #i ∨
+                           ∃∃K,V,V2. ⬇*[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 &
+                                     ⬆*[⫯i] V2 ≡ T2.
+#h #G #L #T2 #i #H elim (cpm_inv_lref1_drops … H) -H *
+[ /2 width=1 by or_introl/
+| /3 width=6 by ex3_3_intro, or_intror/
+| #m #K #V1 #V2 #_ #_ #_ #H destruct
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_lift.ma
deleted file mode 100644
index bebe3429f..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_lift.ma
+++ /dev/null
@@ -1,112 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "ground_2/ynat/ynat_max.ma".
-include "basic_2/substitution/drop_drop.ma".
-include "basic_2/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
-
-(* Relocation properties ****************************************************)
-
-(* Basic_1: includes: pr0_lift pr2_lift *)
-lemma cpr_lift: ∀G. d_liftable (cpr G).
-#G #K #T1 #T2 #H elim H -G -K -T1 -T2
-[ #I #G #K #L #b #l #k #_ #U1 #H1 #U2 #H2
-  >(lift_mono … H1 … H2) -H1 -H2 //
-| #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #b #l #k #HLK #U1 #H #U2 #HWU2
-  elim (lift_inv_lref1 … H) * #Hil #H destruct
-  [ elim (lift_trans_ge … HVW2 … HWU2) -W2 /2 width=1 by ylt_fwd_le_succ1/ #W2 #HVW2 #HWU2
-    elim (drop_trans_le … HLK … HKV) -K /2 width=2 by ylt_fwd_le/ #X #HLK #H
-    elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil
-    #K #Y #HKV #HVY #H destruct /3 width=9 by cpr_delta/
-  | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2
-    lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hil /3 width=6 by cpr_delta, drop_inv_gen/
-  ]
-| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #b #l #k #HLK #U1 #H1 #U2 #H2
-  elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
-  elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=6 by cpr_bind, drop_skip/
-| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #b #l #k #HLK #U1 #H1 #U2 #H2
-  elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
-  elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpr_flat/
-| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #b #l #k #HLK #U1 #H #U2 #HTU2
-  elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
-  elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpr_zeta, drop_skip/
-| #G #K #V #T1 #T2 #_ #IHT12 #L #b #l #k #HLK #U1 #H #U2 #HTU2
-  elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpr_eps/
-| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #b #l #k #HLK #X1 #HX1 #X2 #HX2
-  elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
-  elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
-  elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct
-  elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=6 by cpr_beta, drop_skip/
-| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #b #l #k #HLK #X1 #HX1 #X2 #HX2
-  elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
-  elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
-  elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct
-  elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct
-  elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=6 by cpr_theta, drop_skip/
-]
-qed.
-
-(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
-lemma cpr_inv_lift1: ∀G. d_deliftable_sn (cpr G).
-#G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #i #G #L #K #b #l #k #_ #T1 #H
-  [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
-  | elim (lift_inv_lref2 … H) -H * #Hil #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
-  | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
-  ]
-| #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #b #l #k #HLK #T1 #H
-  elim (lift_inv_lref2 … H) -H * #Hil #H destruct
-  [ elim (drop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
-    elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
-    elim (lift_trans_le … HUV2 … HVW2) -V2 // <yminus_succ2 <yplus_inj >yplus_SO2 >ymax_pre_sn /3 width=8 by cpr_delta, ylt_fwd_le_succ1, ex2_intro/
-  | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi
-    lapply (yle_inv_inj … Hmi) -Hmi #Hmi
-    lapply (drop_conf_ge … HLK … HLV ?) -L // #HKLV
-    elim (lift_split … HVW2 l (i - k + 1)) -HVW2 [2,3,4: /2 width=1 by yle_succ_dx, le_S_S/ ] -Hil -Hlim
-    #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O
-    /3 width=8 by cpr_delta, ex2_intro/
-  ]
-| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #b #l #k #HLK #X #H
-  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
-  elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=6 by cpr_bind, drop_skip, lift_bind, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #b #l #k #HLK #X #H
-  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHV12 … HLK … HWV1) -V1
-  elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=6 by cpr_flat, lift_flat, ex2_intro/
-| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #b #l #k #HLK #X #H
-  elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU1 (K.ⓓW1) b  … HTU1) /2 width=1 by drop_skip/ -L -U1 #T #HTU #HT1
-  elim (lift_div_le … HU2 … HTU) -U /3 width=6 by cpr_zeta, ex2_intro/
-| #G #L #V #U1 #U2 #_ #IHU12 #K #b #l #k #HLK #X #H
-  elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
-  elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpr_eps, ex2_intro/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #b #l #k #HLK #X #HX
-  elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
-  elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
-  elim (IHV12 … HLK … HV01) -V1
-  elim (IHT12 (K.ⓛW0) b … HT01) -T1 /2 width=1 by drop_skip/
-  elim (IHW12 … HLK … HW01) -W1 /4 width=7 by cpr_beta, lift_flat, lift_bind, ex2_intro/
-| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #b #l #k #HLK #X #HX
-  elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
-  elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
-  elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
-  elim (IHT12 (K.ⓓW0) b … HT01) -T1 /2 width=1 by drop_skip/ #T3 #HT32 #HT03
-  elim (IHW12 … HLK … HW01) -W1
-  elim (lift_trans_le … HV3 … HV2) -V
-  /4 width=9 by cpr_theta, lift_flat, lift_bind, ex2_intro/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma
index 98c2b491f..fe9afa3a8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma
@@ -60,7 +60,7 @@ qed-.
 (* Inversion lemmas with generic slicing for local environments *************)
 
 (* Basic_2A1: includes: cpx_inv_lift1 *)
-lemma cpx_inv_lift1: ∀h,G. d_deliftable2_sn (cpx h G).
+lemma cpx_inv_lifts: ∀h,G. d_deliftable2_sn (cpx h G).
 #h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1
 elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1
 /3 width=4 by ex2_intro, ex_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma
index c2e3d8ad7..cabba2b41 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma
@@ -17,6 +17,8 @@ include "basic_2/rt_transition/cpx.ma".
 
 (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
 
+(* Properties with restricted refinement for local environments *************)
+
 lemma lsubr_cpx_trans: ∀h,G. lsub_trans … (cpx h G) lsubr.
 #h #G #L1 #T1 #T2 * /3 width=4 by lsubr_cpg_trans, ex_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt
index 642ca8aa2..32cf5942c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt
@@ -1,5 +1,5 @@
 cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma
 cpx.ma cpx_simple.ma cpx_drops.ma cpx_lsubr.ma
 lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma 
-cpm.ma
-cpr.ma
+cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_cpx.ma
+cpr.ma cpr_drops.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 2aa5021d1..0221fc36f 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
@@ -142,12 +142,13 @@ table {
              [ "cpx_lreq" + "cpx_fqus" + "cpx_llpx_sn" + "cpx_lleq" * ]
           }
         ]
-        [ { "context-sensitive reduction" * } {
-             [ "lpr ( ⦃?,?⦄ ⊢ ➡ ? )" "lpr_drop" + "lpr_lpr" * ]
-             [ "cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )" "cpr_lift" + "cpr_llpx_sn" + "cpr_cir" * ]
+*)
+        [ { "t-bound context-sensitive rt-transition" * } {
+(*             [ "lpr ( ⦃?,?⦄ ⊢ ➡ ? )" "lpr_drop" + "lpr_lpr" * ] *)
+             [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" (* + "cpr_llpx_sn" + "cpr_cir" *) * ]
+             [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_cpx" * ]
           }
         ]
-*)
         [ { "uncounted context-sensitive rt-transition" * } {
              [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" * ]
              [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
-- 
2.39.2