From b5507c449ba38a76666a35664f9cf4e1953ad8ec Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Fri, 24 Dec 2021 10:52:38 +0100
Subject: [PATCH] update in ground

+ uniform total relocations
---
 .../lambdadelta/ground/relocation/tr_id.ma    | 30 ++++++++++++++++
 .../lambdadelta/ground/relocation/tr_uni.ma   | 34 +++++++++++++++++++
 .../lambdadelta/ground/web/ground_src.tbl     |  2 ++
 3 files changed, 66 insertions(+)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_id.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id.ma
new file mode 100644
index 000000000..9b421ee43
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/element_i_0.ma".
+include "ground/relocation/tr_pn.ma".
+
+(* IDENTITY ELEMENT FOR TOTAL RELOCATION MAPS *******************************)
+
+corec definition tr_id: tr_map ≝ ⫯tr_id.
+
+interpretation
+  "identity element (total relocation streams)"
+  'ElementI = (tr_id).
+
+(* Basic constructions (specific) *******************************************)
+
+lemma tr_id_unfold: ⫯𝐢 = 𝐢.
+<(stream_unfold … (𝐢)) in ⊢ (???%); //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma
new file mode 100644
index 000000000..b57b05a94
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/nat_succ.ma".
+include "ground/notation/functions/element_u_1.ma".
+include "ground/relocation/tr_id.ma".
+
+(* UNIFORM ELEMENTS FOR TOTAL RELOCATION MAPS *******************************)
+
+definition tr_uni (n:nat): tr_map ≝ ↑n ⨮ 𝐢.
+
+interpretation
+  "uniform elements (total relocation maps)"
+  'ElementU n = (tr_uni n).
+
+(* Basic constructions ******************************************************)
+
+lemma tr_uni_zero: 𝐢 = 𝐮❨𝟎❩.
+<tr_id_unfold //
+qed.
+
+lemma tr_uni_succ (n): ↑𝐮❨n❩ = 𝐮❨↑n❩.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index a903cf088..6a4e3dcf9 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -30,6 +30,8 @@ table {
         }
       ]
       [ { "total relocation" * } {
+          [ "tr_uni ( 𝐮❨?❩ )" * ]
+          [ "tr_id ( 𝐢 ) " * ]
           [ "tr_compose ( ?∘? )" "tr_compose_pn" * ]
           [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pap" * ]
           [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ]
-- 
2.39.2