X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Funwind%2Funwind2_rmap_eq.ma;h=b93aabf0ffb8316da2e18428b92a6a9b54798acd;hb=119da3f9ce130f7c4e8b23fcc491d221472ad657;hp=7ca7f175c40dc5e9a6e9f3e0d2ebcce8539e6ded;hpb=ad6182251b8192ee7d25c53156afbce35e3715b6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
index 7ca7f175c..b93aabf0f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
@@ -13,30 +13,24 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_rmap.ma".
+include "delayed_updating/unwind/preunwind2_rmap_eq.ma".
 include "ground/relocation/tr_uni_compose.ma".
-include "ground/relocation/tr_compose_eq.ma".
-include "ground/relocation/tr_pn_eq.ma".
 include "ground/arith/nat_rplus_pplus.ma".
 
-(* UNWIND MAP FOR PATH ******************************************************)
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
 
-(* Constructions with stream_eq *********************************************)
+(* Constructions with tr_map_eq *********************************************)
 
 lemma unwind2_rmap_eq_repl (p):
       stream_eq_repl … (λf1,f2. ▶[f1]p ≗ ▶[f2]p).
 #p elim p -p //
-* [ #n ] #p #IH #f1 #f2 #Hf
-[ /3 width=1 by tr_compose_eq_repl/
-| /2 width=1 by/
-| /3 width=1 by tr_push_eq_repl/
-| /2 width=1 by/
-| /2 width=1 by/
-]
+#l #p #IH #f1 #f2 #Hf
+/3 width=1 by preunwind2_rmap_eq_repl/
 qed-.
 
-lemma tls_unwind2_rmap_d_sn (f) (p) (m) (n):
-      ⇂*[m+n]▶[f]p ≗ ⇂*[m]▶[f](𝗱n◗p).
-#f #p #m #n
-<unwind2_rmap_d_sn >nrplus_inj_dx
+lemma tls_unwind2_rmap_d_dx (f) (p) (h) (k):
+      ⇂*[h+k]▶[f]p ≗ ⇂*[h]▶[f](p◖𝗱k).
+#f #p #h #k
+<unwind2_rmap_d_dx >nrplus_inj_dx
 /2 width=1 by tr_tls_compose_uni_dx/
 qed.