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=5e607ac373e56b79c44d2d545da8168b645504b2;hpb=6c52017b15171aa20ddfd01c1bbf3cc22a86c81c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
index 5e607ac37..0f367b218 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
@@ -1,18 +1,19 @@
+(**) (* reverse include *)
 include "ground/arith/nat_rplus_pplus.ma".
-include "ground/relocation/nap.ma".
-include "ground/notation/functions/apply_2.ma".
+include "ground/relocation/tr_pn_eq.ma".
 include "ground/relocation/tr_compose_pn.ma".
-include "ground/relocation/tr_pap_tls.ma".
+include "ground/relocation/nap.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):
@@ -24,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.
@@ -69,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.