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 "delayed_updating/substitution/lift_gen_eq.ma".
16 include "delayed_updating/syntax/path_head.ma".
17 include "delayed_updating/syntax/path_reverse.ma".
18 include "ground/lib/stream_eq_eq.ma".
20 (* LIFT MAP FOR PATH ********************************************************)
22 (* Constructions with path_head *********************************************)
24 lemma tls_plus_lift_rmap_reverse_closed (f) (q) (n) (k):
26 ⇂*[k]f ≗ ⇂*[n+k]↑[qᴿ]f.
29 <(eq_inv_path_empty_head … Hq) -n //
30 | #l #q #IH #n @(nat_ind_succ … n) -n //
31 #n #_ #k cases l [ #m ]
33 elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hp <nrplus_inj_sn
35 @(stream_eq_trans … (tls_lift_rmap_d_dx …))
36 >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
37 >nsucc_unfold /2 width=1 by/
39 elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
40 <reverse_lcons <lift_rmap_m_dx /2 width=1 by/
42 elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
43 <reverse_lcons <lift_rmap_L_dx <nplus_succ_sn /2 width=1 by/
45 elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
46 <reverse_lcons <lift_rmap_A_dx /2 width=2 by/
48 elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
49 <reverse_lcons <lift_rmap_S_dx /2 width=2 by/
54 lemma tls_lift_rmap_closed (f) (q) (n):
59 /2 width=1 by tls_plus_lift_rmap_reverse_closed/