From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 1 Mar 2022 00:12:44 +0000 (+0100)
Subject: update in ground
X-Git-Tag: make_still_working~85
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f717d9ef23433a96583a1bc8ae6b903689d5f033;p=helm.git

update in ground

+ minor corrections and additions
---

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
index 468f306de..d6a9a5742 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
@@ -36,11 +36,11 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma stream_hd_cons (A) (a) (t):
+lemma stream_hd_lcons (A) (a) (t):
       a = ⇃{A}(a⨮t).
 // qed.
 
-lemma stream_tl_cons (A) (a) (t):
+lemma stream_tl_lcons (A) (a) (t):
       t = ⇂{A}(a⨮t).
 // qed.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
index eb7210e22..f66c8a63f 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
@@ -52,3 +52,7 @@ lemma stream_tls_swap (A) (n) (t):
 lemma stream_tls_unit (A) (t):
       ⇂t = ⇂*{A}[𝟏]t.
 // qed.
+
+lemma stream_tls_succ_lcons (A) (n) (a) (t):
+      ⇂*[n]t = ⇂*{A}[↑n](a⨮t).
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pushs.ma
new file mode 100644
index 000000000..0f9174b64
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pushs.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_compose_pn.ma".
+
+(* COMPOSITION FOR TOTAL RELOCATION MAPS ************************************)
+
+(* Constructions with tr_pushs **********************************************)
+
+lemma tr_compose_pushs_bi (n) (f2) (f1):
+      (⫯*[n](f2∘f1)) = (⫯*[n]f2)∘(⫯*[n]f1).
+#n @(nat_ind_succ … n) -n //
+#n #IH #f1 #f2
+<tr_pushs_succ <tr_pushs_succ <tr_pushs_succ
+<tr_compose_push_bi //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
index 1a7947f38..2ff52deec 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
@@ -21,13 +21,10 @@ include "ground/arith/nat_rplus_pplus.ma".
 
 (* Advanced constructions with stream_tls ***********************************)
 
-lemma tr_compose_tls (i) (f2) (f1):
-      (⇂*[f1@❨i❩]f2)∘⇂*[i]f1 = ⇂*[i](f2∘f1).
-#i elim i -i
-[ #f2 * #p1 #f1 //
-| #i #IH #f2 * #p1 #f1
-  >nsucc_inj <stream_tls_swap <stream_tls_swap
-  <tr_pap_succ >nrplus_inj_dx >nrplus_inj_sn
-  <tr_compose_unfold <IH -IH //
-]
+lemma tr_compose_tls (p) (f1) (f2):
+      (⇂*[f1@❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
+#p elim p -p [| #p #IH ] * #q1 #f1 #f2 //
+<tr_compose_unfold <tr_pap_succ
+>nsucc_inj <stream_tls_succ_lcons <stream_tls_succ_lcons
+<IH -IH >nrplus_inj_dx >nrplus_inj_sn <stream_tls_plus //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index a4a802c68..d04a95414 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -32,7 +32,7 @@ table {
       [ { "total relocation" * } {
           [ "tr_uni ( 𝐮❨?❩ )" "tr_uni_pap" "tr_uni_compose" * ]
           [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" "tr_id_compose" * ]
-          [ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pap" "tr_compose_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_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
           [ "tr_pushs ( ⫯*[?]? )" * ]
           [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_eq" "tr_pn_hdtl" "tr_pn_tls" * ]