From 7c9d99dfb049d726491b71f07ba6a9b088b30166 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 22 Jan 2023 01:05:23 +0100 Subject: [PATCH] wip .... + a situation in which matita falls asleep was detected --- .../relocation/tr_minus_pap.ma | 24 +++++++++++++++++ .../ground/arith/nat_minus_pminus.ma | 27 +++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_minus_pminus.ma 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 f27e43c65..0df2d501f 100644 --- 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 + [ nsucc_inj /2 width=1 by/ + | nsucc_inj >nsucc_inj