matita/matita/contribs/lambdadelta/delayed_updating/unwind/xap.ma

   1 include "delayed_updating/unwind/nap.ma".
   2 include "ground/notation/functions/apply_2.ma".
   3 include "ground/relocation/tr_compose_pn.ma".
   4
   5 definition tr_xap (f) (l:nat): nat ≝
   6            (⫯f)@↑❨l❩.
   7
   8 interpretation
   9   "functional extended application (total relocation maps)"
  10   'Apply f l = (tr_xap f l).
  11
  12 lemma tr_xap_unfold (f) (l):
  13       (⫯f)@↑❨l❩ = f＠❨l❩.
  14 // qed.
  15
  16 lemma tr_xap_zero (f):
  17       (𝟎) = f＠❨𝟎❩.
  18 // qed.
  19
  20 lemma tr_xap_ninj (f) (p):
  21       ninj (f＠⧣❨p❩) = f＠❨ninj p❩.
  22 // qed.
  23
  24 lemma tr_compose_xap (f2) (f1) (l):
  25       f2＠❨f1＠❨l❩❩ = (f2∘f1)＠❨l❩.
  26 #f2 #f1 #l
  27 <tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
  28 >tr_compose_nap >tr_compose_push_bi //
  29 qed.
  30
  31 lemma tr_uni_xap_succ (n) (m):
  32       ↑m + n = 𝐮❨n❩＠❨↑m❩.
  33 #n #m
  34 <tr_xap_unfold
  35 <tr_nap_push <tr_uni_nap //
  36 qed.
  37
  38 lemma tr_uni_xap (n) (m):
  39       𝐮❨n❩＠❨m❩ ≤ m+n.
  40 #n #m @(nat_ind_succ … m) -m //
  41 qed.
  42
  43 lemma tr_xap_push (f) (l):
  44       ↑(f＠❨l❩) = (⫯f)＠❨↑l❩.
  45 #f #l
  46 <tr_xap_unfold <tr_xap_unfold
  47 <tr_nap_push //
  48 qed.
  49
  50 lemma tr_xap_pushs_le (f) (n) (m):
  51       m ≤ n → m = (⫯*[n]f)＠❨m❩.
  52 #f #n #m #Hmn
  53 <tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
  54 /2 width=1 by nlt_succ_dx/
  55 qed-.