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 (p) (f1) (f2):
25 (⇂*[f1@❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
26 #p elim p -p [| #p #IH ] * #q1 #f1 #f2 //
27 <tr_compose_unfold <tr_pap_succ
28 >nsucc_inj <stream_tls_succ_lcons <stream_tls_succ_lcons
29 <IH -IH >nrplus_inj_dx >nrplus_inj_sn <stream_tls_plus //