update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_compose_pn.ma

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 e6e9ae515b71696c83f0be08d7278ebb0485aa41..ec92283789ce8f9b08ebbd383b7c68cf82cf6461 100644 (file)
--- 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):
@@ -43,7 +61,7 @@ qed-.
 (*** compose_inv_S1 *)
 lemma tr_compose_inv_next_sn (f2) (f1):
       ∀f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
-      ∧∧ ↑(f2@❨p1❩) = p & f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+      ∧∧ ↑(f2＠⧣❨p1❩) = p & f2∘(p1⨮f1) = f2＠⧣❨p1❩⨮f.
 #f2 #f1 #f #p1 #p
 <tr_compose_unfold #H destruct
 /2 width=1 by conj/