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) (p) (n) (k):
26 ⇂*[k]↑[pᴿ]f ≗ ⇂*[n+k]↑[qᴿ]f.
29 elim (eq_inv_list_empty_append … Hp) -Hp #Hn #H0 destruct
30 <path_head_empty in Hn; #Hn
31 <(eq_inv_empty_labels … Hn) -n //
32 | #l #q #IH #p #n @(nat_ind_succ … n) -n //
33 #n #_ #k cases l [ #m ]
34 [ <path_head_d_sn <list_append_lcons_sn #Hp
35 elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp <nrplus_inj_sn
37 @(stream_eq_trans … (tls_lift_rmap_d_dx …))
38 >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
39 >nsucc_unfold /2 width=1 by/
40 | <path_head_m_sn <list_append_lcons_sn #Hp
41 elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
42 <reverse_lcons <lift_rmap_m_dx /2 width=1 by/
43 | <path_head_L_sn <list_append_lcons_sn #Hp
44 elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
45 <reverse_lcons <lift_rmap_L_dx <nplus_succ_sn /2 width=1 by/
46 | <path_head_A_sn <list_append_lcons_sn #Hp
47 elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
48 <reverse_lcons <lift_rmap_A_dx /2 width=2 by/
49 | <path_head_S_sn <list_append_lcons_sn #Hp
50 elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
51 <reverse_lcons <lift_rmap_S_dx /2 width=2 by/
56 lemma tls_lift_rmap_append_closed (f) (p) (q) (n):
60 >(reverse_reverse p) >(reverse_reverse q)
61 /2 width=1 by tls_plus_lift_rmap_reverse_closed/