update in ground

+ additions to tr_compose

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc
index ba3287eb6d5193fc1b579433f54d58854fde1f61..a0aba6e512d84bafbcfc0d3af918d9bcfd0f77f3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc
+++ b/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc
@@ -3,14 +3,6 @@ lemma pippo (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❩.
 

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
index b2f042c1f20faeae78cba32d601ea94e3952b311..eb7210e2213d2b62bf20fc83c9c35516479a1965 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
@@ -46,3 +46,9 @@ qed.
 lemma stream_tls_swap (A) (n) (t):
       (⇂*[n]⇂t) = ⇂*{A}[↑n]t.
 // qed.
+
+(* Advanced constructions ***************************************************)
+
+lemma stream_tls_unit (A) (t):
+      ⇂t = ⇂*{A}[𝟏]t.
+// qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_compose.ma
new file mode 100644 (file)
index 0000000..518154d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_compose.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_id_pap.ma".
+include "ground/relocation/tr_compose_pap.ma".
+include "ground/relocation/tr_pap_eq.ma".
+
+(* IDENTITY ELEMENT FOR TOTAL RELOCATION MAPS *******************************)
+
+(* Coonstructions with tr_compose *******************************************)
+
+lemma tr_compose_id_sn (f):
+      f ≗ 𝐢∘f.
+#f @nstream_eq_inv_ext #q //
+qed.
+
+lemma tr_compose_id_dx (f):
+      f ≗ f∘𝐢.
+#f @nstream_eq_inv_ext #q //
+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
index 0648738191ed59e9f95f07bcd955c1827e2482c6..3d329e795f23b79be89abb02e386945bdaed02e5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
@@ -13,11 +13,35 @@
 (**************************************************************************)
 
 include "ground/relocation/tr_uni_pap.ma".
-include "ground/relocation/tr_compose_pap.ma".
-include "ground/relocation/tr_pap_eq.ma".
+include "ground/relocation/tr_id_compose.ma".
+include "ground/relocation/tr_compose_pn.ma".
+include "ground/lib/stream_hdtl_eq.ma".
 
 (* UNIFORM ELEMENTS FOR TOTAL RELOCATION MAPS *******************************)
 
+(* Constructions with tr_compose and tr_tl **********************************)
+
+lemma tr_tl_compose_uni_sn (n) (f):
+      ⇂f ≗ ⇂(𝐮❨n❩∘f).
+#n @(nat_ind_succ … n) -n //
+/2 width=1 by stream_tl_eq_repl/
+qed.
+
+(* Constructions with tr_compose and tr_tls *********************************)
+
+lemma tr_tl_compose_uni_dx (f) (n):
+      ⇂*[↑n]f ≗ ⇂(f∘𝐮❨n❩).
+// qed.
+
+lemma tr_tls_compose_uni_dx (f) (p) (n):
+      ⇂*[p+n]f ≗ ⇂*[p](f∘𝐮❨n❩).
+#f #p elim p -p [| #p #IH ] #n
+[ <nrplus_unit_sn //
+| <nrplus_succ_sn >nsucc_inj >nsucc_inj
+  /2 width=3 by stream_tl_eq_repl/
+]
+qed.
+
 (* Main constructions with tr_compose and tr_tls ****************************)
 
 theorem tr_compose_uni_dx (f) (p):

diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 485443977aaea0681948b81a269e7c2dfc0b3f14..a4a802c6887684e841454b8d4647de2a61a9cf46 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -31,7 +31,7 @@ table {
       ]
       [ { "total relocation" * } {
           [ "tr_uni ( 𝐮❨?❩ )" "tr_uni_pap" "tr_uni_compose" * ]
-          [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" * ]
+          [ "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_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
           [ "tr_pushs ( ⫯*[?]? )" * ]