From d71e53021b0c17e1a00c2d623e7139c6d18069d5 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 7 Aug 2018 18:41:42 +0200
Subject: [PATCH] commit in ground_2, static_2, basic_2, apps_2

+ first steps towards cnv_cpms_conf_aux
+ examples reconstructed
+ additions in the relocation library
+ addition in the arith library
---
 .../examples/ex_sta_ldec.etc}                 |  0
 .../lambdadelta/apps_2/examples/ex_cnv_eta.ma | 52 ++++++++++++++++
 .../apps_2/examples/ex_fpbg_refl.ma           | 33 +++++-----
 .../lambdadelta/apps_2/examples/ex_snv_eta.ma | 61 -------------------
 .../lambdadelta/apps_2/web/apps_2_src.tbl     |  2 +-
 .../basic_2/dynamic/cnv_cpm_conf.ma           |  5 +-
 .../basic_2/dynamic/cnv_cpm_trans.ma          |  3 +-
 .../basic_2/dynamic/cnv_cpms_conf.ma          | 43 +++++++++++++
 .../basic_2/dynamic/cnv_preserve_far.ma       | 14 +++++
 .../basic_2/notation/relations/predstar_7.ma  | 19 ++++++
 .../basic_2/rt_computation/fsb_fpbg.ma        |  9 +++
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  2 +-
 .../lambdadelta/ground_2/lib/arith.ma         | 13 ++--
 .../lambdadelta/ground_2/lib/arith_2b.ma      | 39 ++++++++++++
 .../lambdadelta/ground_2/web/ground_2_src.tbl |  2 +-
 .../matita/contribs/lambdadelta/partial.txt   | 10 +--
 .../lambdadelta/static_2/relocation/lifts.ma  |  9 +++
 17 files changed, 220 insertions(+), 96 deletions(-)
 rename matita/matita/contribs/lambdadelta/apps_2/{examples/ex_sta_ldec.ma => etc/examples/ex_sta_ldec.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/apps_2/examples/ex_snv_eta.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_7.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_sta_ldec.ma b/matita/matita/contribs/lambdadelta/apps_2/etc/examples/ex_sta_ldec.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/apps_2/examples/ex_sta_ldec.ma
rename to matita/matita/contribs/lambdadelta/apps_2/etc/examples/ex_sta_ldec.etc
diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
new file mode 100644
index 000000000..f5bc8f427
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/cpms_drops.ma".
+include "basic_2/dynamic/cnv.ma".
+
+(* EXAMPLES *****************************************************************)
+
+(* Extended validy (basic?_2) vs. restricted validity (basic_1) *************)
+
+(* Note: extended validity of a closure, height of cnv_appl > 1 *)
+lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 ![Ⓕ,h].
+#h #p #G #L #s
+@(cnv_appl … 2 p … (⋆s) … (⋆s))
+[ #H destruct
+| /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
+| /4 width=1 by cnv_bind, cnv_zero/
+| /5 width=3 by cpm_cpms, cpm_lref, cpm_ell, lifts_sort/
+| /5 width=5 by cpm_cpms, cpm_bind, cpm_ell, lifts_uni, lifts_sort, lifts_bind/
+]
+qed.
+
+(* Note: restricted validity of the η-expanded closure, height of cnv_appl = 1 **)
+lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![Ⓣ,h].
+#h #p #G #L #s
+@(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2))
+[ /2 width=1 by/
+| /4 width=1 by cnv_sort, cnv_zero, cnv_lref/
+| @cnv_zero
+  @cnv_bind //
+  @(cnv_appl … 1 p … (⋆s) … (⋆s))
+  [ /2 width=1 by/
+  | /2 width=1 by cnv_sort, cnv_zero/
+  | /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/
+  | /2 width=3 by cpms_ell, lifts_sort/
+  | /4 width=5 by cpms_lref, cpms_ell, lifts_uni, lifts_sort, lifts_bind/
+  ]
+| /4 width=3 by cpms_lref, cpms_ell, lifts_sort/
+| /5 width=7 by cpms_ell, lifts_bind, lifts_flat, lifts_push_lref, lifts_push_zero, lifts_sort/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma
index e37f8831f..f15bbd19c 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma
@@ -12,11 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/fpbg_fpbs.ma".
+include "basic_2/rt_computation/fpbs_cpxs.ma".
+include "basic_2/rt_computation/fpbg_fqup.ma".
+include "basic_2/rt_computation/fpbg_fpbs.ma".
 
 (* EXAMPLES *****************************************************************)
 
-(* Reflexivity of proper qrst-computation: the term ApplOmega ***************)
+(* Reflexivity of proper rst-computation: the term ApplOmega ****************)
 
 definition ApplDelta: term → nat → term ≝ λW,s. +ⓛW.ⓐ⋆s.ⓐ#0.#0.
 
@@ -28,27 +30,28 @@ definition ApplOmega3: term → nat → term ≝ λW,s. ⓐ⋆s.(ApplOmega1 W s)
 
 (* Basic properties *********************************************************)
 
-lemma ApplDelta_lift: ∀W1,W2,s,l,k. ⬆[l, k] W1 ≡ W2 →
-                      ⬆[l, k] (ApplDelta W1 s) ≡ (ApplDelta W2 s).
-/5 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed.
+lemma ApplDelta_lifts (f:rtmap):
+                      ∀W1,W2,s. ⬆*[f] W1 ≘ W2 →
+                      ⬆*[f] (ApplDelta W1 s) ≘ (ApplDelta W2 s).
+/5 width=1 by lifts_sort, lifts_lref, lifts_bind, lifts_flat/ qed.
 
-lemma cpr_ApplOmega_12: ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡ ApplOmega2 W s.
-/2 width=1 by cpr_beta/ qed.
+lemma cpr_ApplOmega_12 (h): ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡[h] ApplOmega2 W s.
+/2 width=1 by cpm_beta/ qed.
 
-lemma cpr_ApplOmega_23: ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega2 W s ➡ ApplOmega3 W s.
-#G #L #W1 #s elim (lift_total W1 0 1) #W2 #HW12
-@(cpr_zeta … (ApplOmega3 W2 s)) /4 width=1 by ApplDelta_lift, lift_flat/
-@cpr_flat // @cpr_flat @(cpr_delta … (ApplDelta W1 s) ? 0)
-[3,5,8,10: /2 width=2 by ApplDelta_lift/ |4,9: /2 width=1 by cpr_eps/ |*: skip ]
+lemma cpr_ApplOmega_23 (h): ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega2 W s ➡[h] ApplOmega3 W s.
+#h #G #L #W1 #s elim (lifts_total W1 (𝐔❴1❵)) #W2 #HW12
+@(cpm_zeta … (ApplOmega3 W2 s)) /4 width=1 by ApplDelta_lifts, lifts_flat/
+@cpm_appl // @cpm_appl @(cpm_delta … (ApplDelta W1 s))
+/2 width=1 by ApplDelta_lifts, cpm_eps/
 qed.
 
-lemma cpxs_ApplOmega_13: ∀h,o,G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ➡*[h,o] ApplOmega3 W s.
-/4 width=3 by cpxs_strap1, cpr_cpx/ qed.
+lemma cpxs_ApplOmega_13 (h): ∀G,L,W,s. ⦃G, L⦄ ⊢ ApplOmega1 W s ⬈*[h] ApplOmega3 W s.
+/4 width=4 by cpxs_strap1, cpm_fwd_cpx/ qed.
 
 lemma fqup_ApplOmega_13: ∀G,L,W,s. ⦃G, L, ApplOmega3 W s⦄ ⊐+ ⦃G, L, ApplOmega1 W s⦄.
 /2 width=1 by/ qed.
 
 (* Main properties **********************************************************)
 
-theorem fpbg_refl: ∀h,o,G,L,W,s. ⦃G, L, ApplOmega1 W s⦄ >≡[h,o] ⦃G, L, ApplOmega1 W s⦄.
+theorem fpbg_refl (h) (o): ∀G,L,W,s. ⦃G, L, ApplOmega1 W s⦄ >[h,o] ⦃G, L, ApplOmega1 W s⦄.
 /3 width=5 by fpbs_fpbg_trans, fqup_fpbg, cpxs_fpbs/ qed.
diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_snv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_snv_eta.ma
deleted file mode 100644
index af66f2c97..000000000
--- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_snv_eta.ma
+++ /dev/null
@@ -1,61 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/dynamic/snv.ma".
-
-(* EXAMPLES *****************************************************************)
-
-(* Extended validy (basic?_2) vs. restricted validity (basic_1) *************)
-
-(* extended validity of a closure, last arg of snv_appl > 1 *)
-lemma snv_extended: ∀h,o,a,G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{a}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 ¡[h, o].
-#h #o #a #G #L #s elim (deg_total h o s)
-#d #Hd @(snv_appl … a … (⋆s) … (⋆s) (0+1+1))
-[ /4 width=5 by snv_lref, drop_drop_lt/
-| /4 width=13 by snv_bind, snv_lref/
-| /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/
-| @(lstas_scpds … (d+1+1))
-  /5 width=11 by lstas_bind, lstas_succ, da_bind, da_ldec, da_sort, lift_bind/
-]
-qed.
-
-(* restricted validity of the η-expanded closure, last arg of snv_appl = 1 **)
-lemma snv_restricted: ∀h,o,a,G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{a}⋆s.⋆s.ⓛⓛ{a}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ¡[h, o].
-#h #o #a #G #L #s elim (deg_total h o s)
-#d #Hd @(snv_appl … a … (⋆s) … (ⓐ#0.#2) (0+1))
-[ /4 width=5 by snv_lref, drop_drop_lt/
-| @snv_lref [4: // |1,2,3: skip ]
-  @snv_bind //
-  @(snv_appl … a … (⋆s) … (⋆s) (0+1))
-  [ @snv_lref [4: // |1,2,3: skip ] //
-  | @snv_lref [4: /2 width=1 by drop_drop_lt/ |1,2,3: skip ] @snv_bind //
-  | @(lstas_scpds … (d+1)) /3 width=6 by da_sort, da_ldec, lstas_succ/
-  | @(lstas_scpds … (d+1)) /3 width=8 by lstas_succ, lstas_bind, drop_drop, lift_bind/
-    @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ] /3 width=1 by da_sort, da_bind/
-  ]
-| /5 width=6 by lstas_scpds, lstas_succ, da_ldec, da_sort, drop_drop_lt/
-| @(lstas_scpds … (d+1+1)) //
-  [ @da_ldec [3: // |1,2: skip ]
-    @da_bind @da_flat @da_ldec [3: /2 width=1 by drop_drop_lt/ |1,2: skip ]
-    /3 width=1 by da_sort, da_bind/
-  | @lstas_succ [4: // |1,2: skip ]
-    [2: @lstas_bind | skip ]
-    [2: @lstas_appl | skip ]
-    [2: @lstas_zero
-        [4: /2 width=1 by drop_drop_lt/ |5: /2 width=2 by lstas_bind/ |*: skip ]
-    |1: skip ]
-    /4 width=2 by lift_flat, lift_bind, lift_lref_ge_minus, lift_lref_lt/
-  ]
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
index 1966269f1..34cf9f851 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
@@ -69,7 +69,7 @@ table {
    class "red"
    [ { "examples" * } {
         [ { "terms with special features" * } {
-             [ (* "ex_sta_ldec" + *) "ex_cpr_omega" (* + "ex_fpbg_refl" + "ex_snv_eta" *) * ]
+             [ "ex_cpr_omega" + "ex_fpbg_refl" + "ex_cnv_eta" * ]
           }
         ]
      }
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
index 160d23f88..70398eaac 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/lib/arith_2b.ma".
 include "basic_2/rt_transition/lpr_lpr.ma".
 include "basic_2/rt_computation/cpms_lsubr.ma".
 include "basic_2/rt_computation/cpms_fpbg.ma".
@@ -327,7 +328,7 @@ elim (cnv_cpms_strip_lpr_far … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2
 elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
 -L0 -V0 -T0 -X0 #U #HVU #HTU
 lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
-lapply (cpms_trans … HT1 … HTU) -T <arith_l #H1
+lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
 /3 width=3 by cpms_eps, ex2_intro/
 qed-.
 
@@ -364,7 +365,7 @@ elim (cnv_cpms_strip_lpr_far … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2
 elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
 -L0 -V0 -T0 -X0 #U #HVU #HTU
 lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
-lapply (cpms_trans … HT1 … HTU) -T <arith_l #H1
+lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
 /2 width=3 by ex2_intro/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
index a40f4fa60..ac40d7823 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/lib/arith_2b.ma".
 include "basic_2/rt_computation/cpms_fpbg.ma".
 include "basic_2/rt_computation/cprs_cprs.ma".
 include "basic_2/rt_computation/lprs_cpms.ma".
@@ -118,7 +119,7 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o):
     elim (IH2 … HXUW1 … HXUT1 … HL12 … HL12) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ] -HXUW1 -HXUT1 -HWU1
     >eq_minus_O // #W0 #H1 #H2 -IH2 -IH1 -L1 -W1 -T1 -U1
     lapply (cprs_trans … HXW21 … H1) -XW1 #H1
-    lapply (cpms_trans … HXT21 … H2) -XT1 <arith_l_eq #H2
+    lapply (cpms_trans … HXT21 … H2) -XT1 <arith_l1 #H2
     /2 width=3 by cnv_cast/
   | #HX -IH2 -HW1 -U1
     lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma
new file mode 100644
index 000000000..ee7c6101b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/dynamic/cnv_cpm_trans.ma".
+include "basic_2/dynamic/cnv_cpm_conf.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Far confluence propery with t-bound rt-computation for terms *************)
+
+fact cnv_cpsms_conf_lpr_aux (a) (h) (o):
+                            ∀G0,L0,T0.
+                            (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+                            (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+                            ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpsms_conf_lpr a h o G1 L1 T1.
+#a #h #o #G #L #T #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT #HT0
+#n1 #T1 * #m11 #m12 #X1 #HnX01 #HX01 #HXT1 #H1
+#n2 #T2 * #m21 #m22 #X2 #HnX02 #HX02 #HXT2 #H2
+#L1 #HL01 #L2 #HL02 destruct
+lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX01 … L0 ?) // #HX1
+lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2
+elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20
+cut (⦃G0,L0,T0⦄ >[h,o] ⦃G0,L0,X1⦄) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *)
+lapply (fpbg_fpbs_trans ??? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=2 by cpms_fwd_fpbs/ ] #H2fpbg
+lapply (cnv_cpms_trans_lpr_far … IH2 … HXZ10 … L0 ?) // #HZ0
+elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01
+elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
+elim (IH1 … HZ01 … HZ02  L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02
+lapply (cpms_trans … HTZ1 … HZ01) -Z1 <arith_l4 #HT1Z
+lapply (cpms_trans … HTZ2 … HZ02) -Z2 <arith_l4 #HT2Z
+/2 width=3 by ex2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma
index e8f2c8e2f..971541b21 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_far.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/notation/relations/predstar_7.ma".
 include "basic_2/rt_computation/fpbg.ma".
 include "basic_2/rt_computation/cpms_fpbs.ma".
 include "basic_2/dynamic/cnv.ma".
@@ -20,6 +21,13 @@ include "basic_2/dynamic/cnv.ma".
 
 (* Inductive premises for the preservation results **************************)
 
+definition cpsms (n) (h) (o): relation4 genv lenv term term ≝ λG,L,T1,T2.
+                 ∃∃n1,n2,T. T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2 = n.
+
+interpretation
+   "context-sensitive parallel stratified t-bound  rt-computarion (term)"
+   'PRedStar n h o G L T1 T2 = (cpsms n h o G L T1 T2).
+
 definition IH_cnv_cpm_trans_lpr (a) (h): relation3 genv lenv term ≝
                                 λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] →
                                 ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡[n,h] T2 →
@@ -48,6 +56,12 @@ definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝
                                 ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
                                 ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
 
+definition IH_cnv_cpsms_conf_lpr (a) (h) (o): relation3 genv lenv term ≝
+                                 λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
+                                 ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h,o] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h,o] T2 →
+                                 ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
+                                 ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+
 (* Properties for preservation **********************************************)
 
 lemma cnv_cpms_trans_lpr_far (a) (h) (o):
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_7.ma
new file mode 100644
index 000000000..bbd49fddd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_7.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 T1 ➡* [ break term 46 n, break term 46 h, break term 46 o ] break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'PRedStar $n $h $o $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma
index 07a9aad5e..cd2c41248 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma
@@ -64,3 +64,12 @@ lemma fsb_ind_fpbg: ∀h,o. ∀Q:relation3 genv lenv term.
 #h #o #Q #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
 /3 width=1 by/
 qed-.
+
+(* Inversion lemmas with proper parallel rst-computation for closures *******)
+
+lemma fsb_fpbg_refl_false (h) (o) (G) (L) (T):
+                          ≥[h,o] 𝐒⦃G, L, T⦄ → ⦃G, L, T⦄ >[h,o] ⦃G, L, T⦄ → ⊥.
+#h #o #G #L #T #H
+@(fsb_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #_ #IH #H
+/2 width=5 by/
+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 143c8ccb1..c58de1441 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
@@ -31,7 +31,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_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_preserve_far" (* + "cnv_preserve" *) * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpms_conf" + "cnv_preserve_far" (* + "cnv_preserve" *) * ]
           }
         ]
      }
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index dfc61de15..24d1d47fb 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -60,12 +60,6 @@ lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
 lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
 // qed.
 
-lemma arith_l (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)).
-* // qed.
-
-lemma arith_l_eq: ∀x. 1 = 1-x+(x-(x-1)).
-// qed.
-
 (* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
 lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
 #x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus //
@@ -152,6 +146,13 @@ lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y -
 lemma minus_le_trans_sn: ∀x1,x2. x1 ≤ x2 → ∀x. x1-x ≤ x2.
 /2 width=3 by transitive_le/ qed.
 
+lemma le_plus_to_minus_l: ∀a,b,c. a + b ≤ c → b ≤ c-a.
+/2 width=1 by le_plus_to_minus_r/
+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-.
+
 (* 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/lib/arith_2b.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma
new file mode 100644
index 000000000..4a1ced644
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.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/lib/arith.ma".
+
+(* ARITHMETICAL PROPERTIES FOR λδ-2B ****************************************)
+
+lemma arith_l4 (m11) (m12) (m21) (m22):
+               m21+m22-(m11+m12) = m21-m11-m12+(m22-(m11-m21)-(m12-(m21-m11))).
+#m11 #m12 #m21 #m22 >minus_plus
+elim (le_or_ge (m11+m12) m21) #Hm1121
+[ lapply (transitive_le m11 ??? Hm1121) // #Hm121
+  lapply (le_plus_to_minus_l … Hm1121) #Hm12211
+  <plus_minus // @eq_f2 // >(eq_minus_O m11 ?) // >(eq_minus_O m12 ?) //
+| >(eq_minus_O m21 ?) // <plus_O_n <minus_plus <commutative_plus
+  elim (le_or_ge m11 m21) #Hm121
+  [ lapply (le_plus_to_minus_comm … Hm1121) #Hm2112
+    >(eq_minus_O m11 ?) // <plus_minus_associative // <minus_le_minus_minus_comm //
+  | >(eq_minus_O m21 ?) // <minus_le_minus_minus_comm //
+  ]
+]
+qed.
+
+lemma arith_l2 (n1) (n2): ↑n2-n1 = 1-n1+(n2-(n1-1)).
+* // qed.
+
+lemma arith_l1: ∀x. 1 = 1-x+(x-(x-1)).
+// 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 310871c3d..33ace356b 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
@@ -59,7 +59,7 @@ table {
         [ { "" * } {
              [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
              [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ]
-             [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ]
+             [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2b" * ]
              [ "ltc" "ltc_ctc" * ]
              [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" * ]
           }
diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt
index 512f0ac54..11b4d4573 100644
--- a/matita/matita/contribs/lambdadelta/partial.txt
+++ b/matita/matita/contribs/lambdadelta/partial.txt
@@ -1,10 +1,4 @@
 ground_2
 static_2
-basic_2/rt_transition
-basic_2/rt_computation
-basic_2/rt_conversion
-basic_2/rt_equivalence
-basic_2/dynamic/
-apps_2/examples/ex_cpr_omega.ma
-apps_2/functional/
-apps_2/models/
+basic_2
+apps_2
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
index 54372cf8f..1d6225393 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
@@ -356,6 +356,15 @@ elim (IHV1 f) -IHV1 #V2 #HV12
 ]
 qed-.
 
+lemma lifts_push_zero (f): ⬆*[⫯f]#O ≘ #0.
+/2 width=1 by lifts_lref/ qed.
+
+lemma lifts_push_lref (f) (i1) (i2): ⬆*[f]#i1 ≘ #i2 → ⬆*[⫯f]#(↑i1) ≘ #(↑i2).
+#f1 #i1 #i2 #H
+elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct
+/3 width=7 by lifts_lref, at_push/
+qed.
+
 lemma lifts_lref_uni: ∀l,i. ⬆*[l] #i ≘ #(l+i).
 #l elim l -l /2 width=1 by lifts_lref/
 qed.
-- 
2.39.2