1 include "ground/arith/nat_rplus_pplus.ma".
2 include "ground/relocation/nap.ma".
3 include "ground/notation/functions/apply_2.ma".
4 include "ground/relocation/tr_compose_pn.ma".
5 include "ground/relocation/tr_pap_tls.ma".
7 definition tr_xap (f) (l:nat): nat ≝
11 "functional extended application (total relocation maps)"
12 'Apply f l = (tr_xap f l).
14 lemma tr_xap_unfold (f) (l):
18 lemma tr_xap_zero (f):
22 lemma tr_xap_ninj (f) (p):
23 ninj (f@⧣❨p❩) = f@❨ninj p❩.
26 lemma tr_xap_succ_nap (f) (n):
32 lemma tr_compose_xap (f2) (f1) (l):
33 f2@❨f1@❨l❩❩ = (f2∘f1)@❨l❩.
35 <tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
36 >tr_compose_nap >tr_compose_push_bi //
39 lemma tr_uni_xap_succ (n) (m):
43 <tr_nap_push <tr_uni_nap //
46 lemma tr_uni_xap (n) (m):
48 #n #m @(nat_ind_succ … m) -m //
51 lemma tr_xap_push (f) (l):
54 <tr_xap_unfold <tr_xap_unfold
58 lemma tr_xap_pushs_le (f) (n) (m):
59 m ≤ n → m = (⫯*[n]f)@❨m❩.
61 <tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
62 /2 width=1 by nlt_succ_dx/
65 lemma tr_xap_plus (n1) (n2) (f):
66 (⇂*[n2]f)@❨n1❩+f@❨n2❩ = f@❨n1+n2❩.
67 * [| #n1 ] // * [| #n2 ] // #f
68 <nrplus_inj_sn <nrplus_inj_dx
69 <nrplus_inj_sn <nrplus_inj_dx