2 (**) (* reverse include *)
3 include "ground/arith/nat_rplus_pplus.ma".
4 include "ground/relocation/tr_pn_eq.ma".
5 include "ground/relocation/tr_compose_pn.ma".
6 include "ground/relocation/nap.ma".
7 include "ground/notation/functions/apply_2.ma".
9 definition tr_xap (f) (l:nat): nat ≝
13 "functional extended application (total relocation maps)"
14 'Apply f l = (tr_xap f l).
16 lemma tr_xap_unfold (f) (l):
20 lemma tr_xap_zero (f):
24 lemma tr_xap_ninj (f) (p):
25 ninj (f@⧣❨p❩) = f@❨ninj p❩.
28 lemma tr_xap_succ_nap (f) (n):
34 lemma tr_compose_xap (f2) (f1) (l):
35 f2@❨f1@❨l❩❩ = (f2∘f1)@❨l❩.
37 <tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
38 >tr_compose_nap >tr_compose_push_bi //
41 lemma tr_uni_xap_succ (n) (m):
45 <tr_nap_push <tr_uni_nap //
48 lemma tr_uni_xap (n) (m):
50 #n #m @(nat_ind_succ … m) -m //
53 lemma tr_xap_push (f) (l):
56 <tr_xap_unfold <tr_xap_unfold
60 lemma tr_xap_pushs_le (f) (n) (m):
61 m ≤ n → m = (⫯*[n]f)@❨m❩.
63 <tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
64 /2 width=1 by nlt_succ_dx/
67 lemma tr_xap_plus (n1) (n2) (f):
68 (⇂*[n2]f)@❨n1❩+f@❨n2❩ = f@❨n1+n2❩.
69 * [| #n1 ] // * [| #n2 ] // #f
70 <nrplus_inj_sn <nrplus_inj_dx
71 <nrplus_inj_sn <nrplus_inj_dx
75 theorem tr_xap_eq_repl (i):
76 stream_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
78 <tr_xap_unfold <tr_xap_unfold
79 /3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/