1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/relocation/tr_compose.ma".
16 include "ground/lib/stream_tls_plus.ma".
17 include "ground/arith/nat_plus_rplus.ma".
18 include "ground/arith/nat_rplus_pplus.ma".
20 (* COMPOSITION FOR TOTAL RELOCATION MAPS ************************************)
22 (* Advanced constructions with stream_tls ***********************************)
24 lemma tr_compose_tls (i) (f2) (f1):
25 (⇂*[f1@❨i❩]f2)∘⇂*[i]f1 = ⇂*[i](f2∘f1).
28 | #i #IH #f2 * #p1 #f1
29 >nsucc_inj <stream_tls_swap <stream_tls_swap
30 <tr_pap_succ >nrplus_inj_dx >nrplus_inj_sn
31 <tr_compose_unfold <IH -IH //