include "ground/relocation/tr_uni_pap.ma".
include "ground/relocation/tr_compose_pap.ma".
-include "ground/relocation/tr_pap_pn.ma".
include "ground/notation/functions/applysucc_2.ma".
include "ground/arith/nat_lt.ma".
include "ground/arith/nat_plus_rplus.ma".
qed.
definition tr_nap (f) (l:nat): nat ≝
- ↓(f@❨↑l❩).
+ ↓(f@⧣❨↑l❩).
interpretation
"functional non-negative application (total relocation maps)"
'ApplySucc f l = (tr_nap f l).
lemma tr_nap_unfold (f) (l):
- ↓(f@❨↑l❩) = f@↑❨l❩.
+ ↓(f@⧣❨↑l❩) = f@↑❨l❩.
// qed.
lemma tr_compose_nap (f2) (f1) (l):