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):