matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_head.ma

   1 include "delayed_updating/substitution/lift_eq.ma".
   2 include "delayed_updating/syntax/path_head.ma".
   3 include "delayed_updating/syntax/path_reverse.ma".
   4 include "ground/relocation/xap.ma".
   5
   6 axiom tr_xap_succ_pos (f) (n):
   7       ↑↓(f＠❨↑n❩) = f＠❨↑n❩.
   8
   9 axiom tr_xap_plus (n1) (n2) (f):
  10       (⇂*[n2]f)＠❨n1❩+f＠❨n2❩ = f＠❨n1+n2❩.
  11
  12 axiom eq_inv_path_empty_head (p) (n):
  13       (𝐞) = ↳[n]p → 𝟎 = n.
  14
  15 lemma lift_path_head (f) (p) (q) (n):
  16       pᴿ = ↳[n](pᴿ●qᴿ) →
  17       ↳[↑[q●p]f＠❨n❩](↑[f](q●p))ᴿ = (↑[↑[q]f]p)ᴿ.
  18 #f #p @(list_ind_rcons … p) -p
  19 [ #q #n #H0
  20   <(eq_inv_path_empty_head … H0) -H0
  21   <path_head_zero //
  22 | #p #l #IH #q #n @(nat_ind_succ …n) -n [| #m #_ ]
  23   [ <reverse_rcons <path_head_zero #H0 destruct
  24   | cases l [ #n ]
  25     [ <reverse_rcons <path_head_d_sn #H0
  26       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
  27       <list_append_assoc <lift_rmap_d_dx <lift_path_d_dx <reverse_rcons
  28       <tr_xap_succ_pos <path_head_d_sn >tr_xap_succ_pos
  29       <lift_path_d_dx >lift_rmap_append <reverse_rcons
  30       @eq_f2 // <(IH … H0) -IH -H0
  31       @eq_f2 // <tr_xap_plus //