-
(**) (* reverse include *)
-include "ground/arith/nat_rplus_pplus.ma".
+include "ground/relocation/tr_pn_eq.ma".
include "ground/relocation/tr_compose_pn.ma".
include "ground/relocation/nap.ma".
-include "ground/notation/functions/apply_2.ma".
+include "ground/notation/functions/at_2.ma".
definition tr_xap (f) (l:nat): nat ≝
- (⫯f)@↑❨l❩.
+ (⫯f)@§❨l❩.
interpretation
"functional extended application (total relocation maps)"
- 'Apply f l = (tr_xap f l).
+ 'At f l = (tr_xap f l).
lemma tr_xap_unfold (f) (l):
- (⫯f)@↑❨l❩ = f@❨l❩.
+ (⫯f)@§❨l❩ = f@❨l❩.
// qed.
lemma tr_xap_zero (f):
// qed.
lemma tr_xap_succ_nap (f) (n):
- ↑(f@↑❨n❩) = f@❨↑n❩.
+ ↑(f@§❨n❩) = f@❨↑n❩.
#f #n
<tr_xap_ninj //
qed.
<nrplus_inj_sn <nrplus_inj_dx
>tr_pap_plus //
qed.
+
+theorem tr_xap_eq_repl (i):
+ stream_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
+#i #f1 #f2 #Hf
+<tr_xap_unfold <tr_xap_unfold
+/3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/
+qed.
+
+lemma tr_nap_plus_dx_xap (f) (m) (n):
+ ⇂*[↑n]f@❨m❩+f@§❨n❩ = f@§❨m+n❩.
+/2 width=1 by tr_nap_eq_repl/
+qed.
+
+lemma tr_nap_plus_sn_xap (f) (m) (n):
+ ⇂*[n]f@§❨m❩+f@❨n❩ = f@§❨m+n❩.
+// qed.
+
+lemma tr_xap_pos (f) (n):
+ n = ↑↓n → f@❨n❩=↑↓(f@❨n❩).
+#f #n #H0 >H0 -H0
+<tr_xap_ninj <nsucc_pnpred //
+qed.