update in ground and delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / xap.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
index 18bcec6a998e7d2b297258c3bd47bc2ff473464a..0f367b218935fe30bb24078908b49b3e678c10d5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
@@ -1,16 +1,19 @@
-include "ground/relocation/nap.ma".
-include "ground/notation/functions/apply_2.ma".
+(**) (* 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/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):
@@ -21,6 +24,12 @@ lemma tr_xap_ninj (f) (p):
       ninj (f＠⧣❨p❩) = f＠❨ninj p❩.
 // qed.
 
+lemma tr_xap_succ_nap (f) (n):
+      ↑(f＠§❨n❩) = f＠❨↑n❩.
+#f #n
+<tr_xap_ninj //
+qed.
+
 lemma tr_compose_xap (f2) (f1) (l):
       f2＠❨f1＠❨l❩❩ = (f2∘f1)＠❨l❩.
 #f2 #f1 #l
@@ -53,3 +62,23 @@ lemma tr_xap_pushs_le (f) (n) (m):
 <tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
 /2 width=1 by nlt_succ_dx/
 qed-.
+
+lemma tr_xap_plus (n1) (n2) (f):
+      (⇂*[n2]f)＠❨n1❩+f＠❨n2❩ = f＠❨n1+n2❩.
+* [| #n1 ] // * [| #n2 ] // #f
+<nrplus_inj_sn <nrplus_inj_dx
+<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.