From 0818b903bf0fb363fab2d7d9f1da64956ea54e81 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 13 Feb 2022 20:14:50 +0100
Subject: [PATCH] update in ground

+ main commutation of tr_compose and tr_uni
---
 .../lambdadelta/ground/etc/relocation/tr.etc  | 29 +++++++++++++++++
 .../ground/relocation/tr_id_pap.ma            |  2 +-
 .../ground/relocation/tr_pap_tls.ma           |  6 ++--
 .../lambdadelta/ground/relocation/tr_uni.ma   |  3 ++
 .../ground/relocation/tr_uni_compose.ma       | 30 ++++++++++++++++++
 .../ground/relocation/tr_uni_pap.ma           | 31 +++++++++++++++++++
 .../lambdadelta/ground/web/ground_src.tbl     |  2 +-
 7 files changed, 98 insertions(+), 5 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_pap.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc
new file mode 100644
index 000000000..ba3287eb6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc
@@ -0,0 +1,29 @@
+lemma pippo (f):
+      f@❨𝟏❩⨮⇂f = f.
+* #p #f //
+qed.
+
+corec lemma tr_compose_id_dx (f):
+            f ≗ f∘𝐢.
+cases tr_id_unfold
+cases tr_compose_unfold
+cases (pippo f) in ⊢ (??%?);
+@stream_eq_cons /2 width=1 by/
+qed.
+
+axiom pippo2 (f) (p):
+      f@❨p❩ + (⇂*[ninj p]f)@❨𝟏❩ = f@❨↑p❩.
+
+lemma tr_uni_tl (n):
+      (𝐢) = ⇂𝐮❨n❩.
+// qed.
+
+axiom tr_uni_tls_pos (p:pnat) (n):
+      (𝐢) = ⇂*[p]𝐮❨n❩.
+(*
+#p #n
+>nsucc_pnpred <stream_tls_swap
+<tr_uni_tl <tr_id_tls
+// qed.
+*)
+
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 34f7ca78c..9a406ba8c 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
@@ -19,7 +19,7 @@ include "ground/relocation/tr_id_pushs.ma".
 
 (* Coonstructions with tr_pap ***********************************************)
 
-lemma tr_pap_id (p):
+lemma tr_id_pap (p):
       p = 𝐢@❨p❩.
 #p >(tr_pushs_id p)
 /2 width=1 by tr_pap_pushs_le/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
index 978d360f6..678792ff5 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
@@ -19,9 +19,9 @@ include "ground/lib/stream_tls.ma".
 
 (* Constructions with stream_tls ********************************************)
 
-lemma tr_pap_plus (i1) (i2) (f):
-      (⇂*[ninj i2]f)@❨i1❩+f@❨i2❩ = f@❨i1+i2❩.
-#i1 #i2 elim i2 -i2
+lemma tr_pap_plus (p1) (p2) (f):
+      (⇂*[ninj p2]f)@❨p1❩+f@❨p2❩ = f@❨p1+p2❩.
+#p1 #p2 elim p2 -p2
 [ * #p #f //
 | #i #IH * #p #f
   <pplus_succ_dx <tr_pap_succ <tr_pap_succ
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma
index b57b05a94..f5c60d12f 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni.ma
@@ -26,6 +26,9 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
+lemma tr_uni_unfold (n): ↑n ⨮ 𝐢 = 𝐮❨n❩.
+// qed.
+
 lemma tr_uni_zero: 𝐢 = 𝐮❨𝟎❩.
 <tr_id_unfold //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
new file mode 100644
index 000000000..064873819
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.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/relocation/tr_uni_pap.ma".
+include "ground/relocation/tr_compose_pap.ma".
+include "ground/relocation/tr_pap_eq.ma".
+
+(* UNIFORM ELEMENTS FOR TOTAL RELOCATION MAPS *******************************)
+
+(* Main constructions with tr_compose and tr_tls ****************************)
+
+theorem tr_compose_uni_dx (f) (p):
+        (𝐮❨f@❨p❩❩∘⇂*[p]f ≗ f∘𝐮❨p❩).
+#f #p
+@nstream_eq_inv_ext #q
+<tr_compose_pap <tr_compose_pap
+<tr_uni_pap <tr_uni_pap
+<tr_pap_plus //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_pap.ma
new file mode 100644
index 000000000..aa99f8dc3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_pap.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_uni.ma".
+include "ground/relocation/tr_id_pap.ma".
+include "ground/arith/nat_rplus_succ.ma".
+
+(* UNIFORM ELEMENTS FOR TOTAL RELOCATION MAPS *******************************)
+
+(* Coonstructions with tr_pap ***********************************************)
+
+lemma tr_uni_pap_unit (n):
+      ↑n = 𝐮❨n❩@❨𝟏❩.
+// qed.
+
+lemma tr_uni_pap (n) (p):
+      p + n = 𝐮❨n❩@❨p❩.
+#n @(nat_ind_succ … n) -n //
+#n #IH * [| #p ] //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 25a425139..485443977 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -30,7 +30,7 @@ table {
         }
       ]
       [ { "total relocation" * } {
-          [ "tr_uni ( 𝐮❨?❩ )" * ]
+          [ "tr_uni ( 𝐮❨?❩ )" "tr_uni_pap" "tr_uni_compose" * ]
           [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" * ]
           [ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pap" "tr_compose_compose" * ]
           [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
-- 
2.39.2