X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_compose_pn.ma;h=acc891d4bf1e1158c25e061ef4d8c0b1b4c01393;hb=01b17de504f0049c15eadcdad651a19adaa954f7;hp=e6e9ae515b71696c83f0be08d7278ebb0485aa41;hpb=80ecd5486c6013f6c297173f41432fd1d93814ef;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
index e6e9ae515..acc891d4b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
@@ -16,20 +16,38 @@ include "ground/relocation/tr_pn_tls.ma".
 include "ground/relocation/tr_pap_pn.ma".
 include "ground/relocation/tr_compose.ma".
 
-(* COMPOSITION FOR PARTIAL RELOCATION MAPS **********************************)
+(* COMPOSITION FOR TOTAL RELOCATION MAPS ************************************)
 
-(* Constructions with tr_push anf tr_next ***********************************)
+(* Constructions with tr_push and tr_next ***********************************)
 
+lemma tr_compose_push_bi (f2) (f1):
+      (⫯(f2∘f1)) = (⫯f2)∘(⫯f1).
+#f2 #f1
+<tr_compose_unfold //
+qed.
+
+lemma tr_compose_push_next (f2) (f1):
+      ↑(f2∘f1) = (⫯f2)∘(↑f1).
+#f2 * #p1 #f1
+<tr_next_unfold <tr_compose_unfold <tr_compose_unfold <tr_next_unfold
+<tr_pap_push >nsucc_inj //
+qed.
+
+(* Note: to be removed *)
 (*** compose_next *)
-lemma tr_compose_next_sn (f2) (f1):
-      ∀f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
+fact tr_compose_next_sn_aux (f2) (f1):
+     ∀f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
 #f2 * #p1 #f1 #f
 <tr_compose_unfold <tr_compose_unfold * -f
 <tr_pap_next 
 /3 width=1 by compose_repl_fwd_dx/
-qed.
+qed-.
+
+lemma tr_compose_next_sn (f2) (f1):
+      ↑(f2∘f1) = (↑f2)∘f1.
+/2 width=1 by tr_compose_next_sn_aux/ qed.
 
-(* Inversions with tr_push anf tr_next **************************************)
+(* Inversions with tr_push and tr_next **************************************)
 
 (*** compose_inv_O2 *)
 lemma tr_compose_inv_push_dx (f2) (f1):