From 775ab35f714568dfcd672f0dd53a00e1ba7382cd Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
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_id_unfold <tr_pap_succ //
+#p >(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 <tr_pushs_succ //
+  | #p #f <npsucc_succ #H0
+    lapply (plt_inv_succ_bi … H0) -H0 #H0
+    lapply (IH … f H0) -IH -H0 #H0
+    <tr_pushs_succ <tr_pap_push //
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 71470225e..05ba00fe4 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -33,7 +33,7 @@ table {
           [ "tr_uni ( 𝐮❨?❩ )" * ]
           [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" * ]
           [ "tr_compose ( ?∘? )" "tr_compose_pn" * ]
-          [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pap" * ]
+          [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
           [ "tr_pushs ( ⫯*[?]? )" * ]
           [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ]
           [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
-- 
2.39.2