From 775ab35f714568dfcd672f0dd53a00e1ba7382cd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 23 Jan 2022 23:00:06 +0100 Subject: [PATCH] update in ground + additions on tr_pap --- .../ground/relocation/tr_id_pap.ma | 8 ++--- .../ground/relocation/tr_pap_pap.ma | 2 ++ .../ground/relocation/tr_pap_pn.ma | 6 ++++ .../ground/relocation/tr_pap_pushs.ma | 36 +++++++++++++++++++ .../lambdadelta/ground/web/ground_src.tbl | 2 +- 5 files changed, 49 insertions(+), 5 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma index 59256fbbb..34f7ca78c 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "ground/relocation/tr_pap.ma". -include "ground/relocation/tr_id.ma". +include "ground/relocation/tr_pap_pushs.ma". +include "ground/relocation/tr_id_pushs.ma". (* IDENTITY ELEMENT FOR TOTAL RELOCATION MAPS *******************************) @@ -21,6 +21,6 @@ include "ground/relocation/tr_id.ma". lemma tr_pap_id (p): p = 𝐢@❨p❩. -#p elim p -p // -#p #IH (tr_pushs_id p) +/2 width=1 by tr_pap_pushs_le/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma index 65cb40105..c3cacbbd4 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma @@ -14,6 +14,8 @@ include "ground/relocation/tr_pap_pat.ma". +(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************) + (* Main inversions **********************************************************) (*** apply_inj *) diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma index 96eaa241f..ce4a0aa32 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma @@ -17,6 +17,12 @@ include "ground/relocation/tr_pap.ma". (* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************) +(* Constructions with tr_push ***********************************************) + +lemma tr_pap_push (f): + ∀i. ↑(f@❨i❩) = (⫯f)@❨↑i❩. +// qed. + (* Constructions with tr_next ***********************************************) (*** apply_S2 *) diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma new file mode 100644 index 000000000..6fe65c8a2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lt.ma". +include "ground/relocation/tr_pushs.ma". +include "ground/relocation/tr_pap_pn.ma". + +(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************) + +(* Constructions with tr_pushs **********************************************) + +lemma tr_pap_pushs_le (n) (p) (f): + p < ↑n → p = (⫯*[n]f)@❨p❩. +#n @(nat_ind_succ … n) -n +[ #p #f #H0 + elim (plt_inv_unit_dx … H0) +| #n #IH * + [ #f #H0