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_eq.ma".
16 include "delayed_updating/syntax/path_head.ma".
17 include "delayed_updating/syntax/path_reverse.ma".
18 include "ground/relocation/xap.ma".
20 (* LIFT FOR PATH ************************************************************)
22 (* Constructions with head for path *****************************************)
24 lemma lift_path_head (f) (p) (q) (n):
26 ↳[↑[q●p]f@❨n❩](↑[f](q●p))ᴿ = (↑[↑[q]f]p)ᴿ.
27 #f #p @(list_ind_rcons … p) -p
29 <(eq_inv_path_empty_head … H0) -H0
31 | #p #l #IH #q #n @(nat_ind_succ …n) -n [| #m #_ ]
32 [ <reverse_rcons <path_head_zero #H0 destruct
34 [ <reverse_rcons <path_head_d_sn #H0
35 elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
36 <list_append_assoc <lift_rmap_d_dx <lift_path_d_dx <reverse_rcons
37 <tr_xap_succ_nap <path_head_d_sn >tr_xap_succ_nap
38 <lift_path_d_dx >lift_rmap_append <reverse_rcons
39 <(IH … H0) -IH -H0 <tr_xap_plus //
40 | <reverse_rcons <path_head_m_sn #H0
41 elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
42 <list_append_assoc <lift_rmap_m_dx <lift_path_m_dx <reverse_rcons
43 <tr_xap_succ_nap <path_head_m_sn >tr_xap_succ_nap
44 <lift_path_m_dx <reverse_rcons
46 | <reverse_rcons <path_head_L_sn #H0
47 elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
48 <list_append_assoc <lift_rmap_L_dx <lift_path_L_dx <reverse_rcons
49 <tr_xap_succ_nap <path_head_L_sn >tr_xap_succ_nap
50 <lift_path_L_dx <reverse_rcons
52 | <reverse_rcons <path_head_A_sn #H0
53 elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
54 <list_append_assoc <lift_rmap_A_dx <lift_path_A_dx <reverse_rcons
55 <tr_xap_succ_nap <path_head_A_sn >tr_xap_succ_nap
56 <lift_path_A_dx <reverse_rcons
58 | <reverse_rcons <path_head_S_sn #H0
59 elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
60 <list_append_assoc <lift_rmap_S_dx <lift_path_S_dx <reverse_rcons
61 <tr_xap_succ_nap <path_head_S_sn >tr_xap_succ_nap
62 <lift_path_S_dx <reverse_rcons