From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 14 Dec 2022 18:37:46 +0000 (+0100)
Subject: update in ground
X-Git-Tag: make_still_working~21
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b05a8a8b1cc518973c30fdbed6a47d7d3ea9d7f0;p=helm.git

update in ground

+ minor addition to relocation
---

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pushs_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pushs_tls.ma
new file mode 100644
index 000000000..fab5dd3e9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pushs_tls.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_pn_hdtl.ma".
+include "ground/lib/stream_tls.ma".
+
+(* ITERATED PUSH FOR TOTAL RELOCATION MAPS **********************************)
+
+(* Constructions with stream_tls ********************************************)
+
+lemma tr_tls_pushs (f) (n):
+      f = ⇂*[n]⫯*[n]f.
+#f #n @(nat_ind_succ … n) -n //
+#n #IH
+<stream_tls_swap <tr_pushs_succ <tr_tl_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 81aeb39e9..12ab26c1d 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -34,7 +34,7 @@ table {
           [ "tr_id ( 𝐢 ) " "tr_id_hdtl" "tr_id_pushs" "tr_id_tls" "tr_id_pap" "tr_id_compose" * ]
           [ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pushs" "tr_compose_pap" "tr_compose_compose" * ]
           [ "tr_pap ( ?＠⧣❨?❩ )" "tr_pap_eq" "tr_pap_hdtl" "tr_pap_hdtl_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
-          [ "tr_pushs ( ⫯*[?]? )" * ]
+          [ "tr_pushs ( ⫯*[?]? )" "tr_pushs_tls" * ]
           [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_eq" "tr_pn_hdtl" "tr_pn_tls" * ]
           [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
         }