wip ....

+ a situation in which matita falls asleep was detected

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma
index f27e43c65e9effc8d30acca4230e3160eeb4bd1c..0df2d501f3734433ca2456ec7f822b6579aae978 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma
@@ -16,6 +16,7 @@ include "delayed_updating/relocation/tr_minus_pn.ma".
 include "ground/relocation/tr_pap_pn.ma".
 include "ground/relocation/tr_pap_lt.ma".
 include "ground/arith/nat_rplus_succ.ma".
+include "ground/arith/nat_minus_pminus.ma".
 include "ground/arith/pnat_le.ma".
 
 (* RIGHT SUBTRACTION FOR TOTAL RELOCATION MAPS ******************************)
@@ -42,3 +43,26 @@ lemma tr_pap_minus_le (n) (p) (f):
   ]
 ]
 qed-.
+
+lemma tr_pap_minus_ge (n:nat) (p:pnat) (f):
+      p + n ≤ f＠⧣❨p❩ →
+      f＠⧣❨p❩-n = (f-n)＠⧣❨p❩.
+#n @(nat_ind_succ … n) -n [| #n #IHn ]
+[ #p #f #_ //
+| #p elim p -p [| #p #IHp ]
+  #f elim (tr_map_split f) * #g #H0 destruct
+  [ <tr_cons_pap_unit <nrplus_unit_sn #H0
+    elim (ple_inv_succ_unit … H0)
+  |2,4:
+    <tr_pap_next <nrplus_succ_dx #Hf
+    lapply (ple_inv_succ_bi … Hf) -Hf #Hf
+    <tr_minus_next_succ >nsucc_inj /2 width=1 by/
+  | <tr_minus_push_succ <tr_pap_push <tr_pap_push <nrplus_succ_sn #Hf
+    lapply (ple_inv_succ_bi … Hf) -Hf #Hf
+    >nsucc_inj >nsucc_inj <IHp -IHp //
+    <nminus_inj_bi
+    [ <nminus_inj_bi 
+      [ <nsucc_inj @eq_f
+(*
+    <nminus_succ_sn //
+*)

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_pminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_pminus.ma
new file mode 100644 (file)
index 0000000..ba850fe
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_pminus.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/arith/pnat_minus.ma".
+include "ground/arith/pnat_lt.ma".
+include "ground/arith/nat_minus.ma".
+
+(* SUBTRACTION FOR NON-NEGATIVE INTEGERS ************************************)
+
+(* Constructions with pminus ************************************************)
+
+lemma nminus_inj_bi (p1) (p2):
+      p2 < p1 →
+      ninj (p1 - p2) = ninj p1 - ninj p2.
+#p2 #p1 #H0 @(plt_ind_alt … H0) -p1 -p2 //
+qed-.