From 1b82038aa813e24e84959526e83dd35d849b51f2 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 22 Jan 2022 20:11:12 +0100
Subject: [PATCH] update in ground

+ additions on tr_id
---
 .../ground/relocation/tr_id_pap.ma            | 26 +++++++++++
 .../ground/relocation/tr_id_pushs.ma          | 25 ++++++++++
 .../lambdadelta/ground/relocation/tr_pushs.ma | 46 +++++++++++++++++++
 .../lambdadelta/ground/web/ground_src.tbl     |  3 +-
 4 files changed, 99 insertions(+), 1 deletion(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pushs.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_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
new file mode 100644
index 000000000..59256fbbb
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/tr_pap.ma".
+include "ground/relocation/tr_id.ma".
+
+(* IDENTITY ELEMENT FOR TOTAL RELOCATION MAPS *******************************)
+
+(* Coonstructions with tr_pap ***********************************************)
+
+lemma tr_pap_id (p):
+      p = 𝐢@❨p❩.
+#p elim p -p //
+#p #IH <tr_id_unfold <tr_pap_succ //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pushs.ma
new file mode 100644
index 000000000..6f54e8bb6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pushs.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/tr_pushs.ma".
+include "ground/relocation/tr_id.ma".
+
+(* IDENTITY ELEMENT FOR TOTAL RELOCATION MAPS *******************************)
+
+(* Constructions with tr_pushs **********************************************)
+
+lemma tr_pushs_id (n): 𝐢 = ⫯*[n]𝐢.
+#n @(nat_ind_succ … n) -n //
+#n #IH <tr_pushs_swap //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pushs.ma
new file mode 100644
index 000000000..9698f7447
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pushs.ma
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/functions/upspoonstar_2.ma".
+include "ground/arith/nat_succ_iter.ma".
+include "ground/relocation/tr_pn.ma".
+
+(* ITERATED PUSH FOR TOTAL RELOCATION MAPS **********************************)
+
+definition tr_pushs (f:tr_map) (n:nat) ≝
+           (tr_push^n) f.
+
+interpretation
+  "iterated push (total relocation maps)"
+  'UpSpoonStar n f = (tr_pushs f n).
+
+(* Basic constructions ******************************************************)
+
+lemma tr_pushs_zero:
+      ∀f. f = ⫯*[𝟎] f.
+// qed.
+
+lemma tr_pushs_push (n):
+      ∀f. ⫯⫯*[n] f = ⫯*[n] ⫯f.
+#n #f @(niter_appl … tr_push)
+qed.
+
+lemma tr_pushs_succ (n):
+      ∀f. ⫯⫯*[n] f = ⫯*[↑n] f.
+#f #n @(niter_succ … tr_push)
+qed.
+
+lemma tr_pushs_swap (n):
+      ∀f. ⫯*[n] ⫯f = ⫯*[↑n] f.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 528c13cf4..71470225e 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -31,9 +31,10 @@ table {
       ]
       [ { "total relocation" * } {
           [ "tr_uni ( 𝐮❨?❩ )" * ]
-          [ "tr_id ( 𝐢 ) " * ]
+          [ "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_pushs ( ⫯*[?]? )" * ]
           [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ]
           [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
         }
-- 
2.39.2