1 include "ground/relocation/tr_uni_pap.ma".
2 include "ground/relocation/tr_compose_pap.ma".
3 include "ground/relocation/tr_pap_pn.ma".
4 include "ground/notation/functions/applysucc_2.ma".
5 include "ground/arith/nat_lt.ma".
6 include "ground/arith/nat_plus_rplus.ma".
7 include "ground/arith/nat_pred_succ.ma".
9 lemma nlt_npsucc_bi (n1) (n2):
10 n1 < n2 → npsucc n1 < npsucc n2.
11 #n1 #n2 #Hn elim Hn -n2 //
12 #n2 #_ #IH /2 width=1 by plt_succ_dx_trans/
15 definition tr_nap (f) (l:nat): nat ≝
19 "functional non-negative application (total relocation maps)"
20 'ApplySucc f l = (tr_nap f l).
22 lemma tr_nap_unfold (f) (l):
26 lemma tr_compose_nap (f2) (f1) (l):
27 f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩.
29 <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
30 <tr_compose_pap <npsucc_pred //
33 lemma tr_uni_nap (n) (m):
37 <tr_uni_pap <nrplus_npsucc_sn //
40 lemma tr_nap_push (f):
41 ∀l. ↑(f@↑❨l❩) = (⫯f)@↑❨↑l❩.
43 <tr_nap_unfold <tr_nap_unfold
44 <tr_pap_push <pnpred_psucc //
47 lemma tr_nap_pushs_lt (f) (n) (m):
48 m < n → m = (⫯*[n]f)@↑❨m❩.
50 <tr_nap_unfold <tr_pap_pushs_le
51 /2 width=1 by nlt_npsucc_bi/