X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fxap.ma;h=0f367b218935fe30bb24078908b49b3e678c10d5;hb=b0c6bbd5db69489a5ebd1b36de6685fa6de441b3;hp=a9096f7e457b289d5528226238a79962d037ce1b;hpb=9fe8259fe25c35d33490d94612023f10dc70a603;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
index a9096f7e4..0f367b218 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
@@ -1,19 +1,19 @@
-
 (**) (* 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):
@@ -25,7 +25,7 @@ lemma tr_xap_ninj (f) (p):
 // qed.
 
 lemma tr_xap_succ_nap (f) (n):
-      ↑(f@↑❨n❩) = f＠❨↑n❩.
+      ↑(f＠§❨n❩) = f＠❨↑n❩.
 #f #n
 <tr_xap_ninj //
 qed.
@@ -70,3 +70,15 @@ lemma tr_xap_plus (n1) (n2) (f):
 <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 (f) (m) (n):
+      ⇂*[↑n]f＠❨m❩+f＠§❨n❩ = f＠§❨m+n❩.
+/2 width=1 by eq_inv_nsucc_bi/
+qed.