1 include "ground/relocation/nap.ma".
2 include "ground/notation/functions/apply_2.ma".
3 include "ground/relocation/tr_compose_pn.ma".
5 definition tr_xap (f) (l:nat): nat ≝
9 "functional extended application (total relocation maps)"
10 'Apply f l = (tr_xap f l).
12 lemma tr_xap_unfold (f) (l):
16 lemma tr_xap_zero (f):
20 lemma tr_xap_ninj (f) (p):
21 ninj (f@⧣❨p❩) = f@❨ninj p❩.
24 lemma tr_compose_xap (f2) (f1) (l):
25 f2@❨f1@❨l❩❩ = (f2∘f1)@❨l❩.
27 <tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
28 >tr_compose_nap >tr_compose_push_bi //
31 lemma tr_uni_xap_succ (n) (m):
35 <tr_nap_push <tr_uni_nap //
38 lemma tr_uni_xap (n) (m):
40 #n #m @(nat_ind_succ … m) -m //
43 lemma tr_xap_push (f) (l):
46 <tr_xap_unfold <tr_xap_unfold
50 lemma tr_xap_pushs_le (f) (n) (m):
51 m ≤ n → m = (⫯*[n]f)@❨m❩.
53 <tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
54 /2 width=1 by nlt_succ_dx/