1 (**) (* reverse include *)
2 include "ground/relocation/tr_pn_eq.ma".
3 include "ground/relocation/tr_compose_pn.ma".
4 include "ground/relocation/nap.ma".
5 include "ground/notation/functions/at_2.ma".
7 definition tr_xap (f) (l:nat): nat ≝
11 "functional extended application (total relocation maps)"
12 'At f l = (tr_xap f l).
14 lemma tr_xap_unfold (f) (l):
18 lemma tr_xap_zero (f):
22 lemma tr_xap_ninj (f) (p):
23 ninj (f@⧣❨p❩) = f@❨ninj p❩.
26 lemma tr_xap_succ_nap (f) (n):
32 lemma tr_compose_xap (f2) (f1) (l):
33 f2@❨f1@❨l❩❩ = (f2∘f1)@❨l❩.
35 <tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
36 >tr_compose_nap >tr_compose_push_bi //
39 lemma tr_uni_xap_succ (n) (m):
43 <tr_nap_push <tr_uni_nap //
46 lemma tr_uni_xap (n) (m):
48 #n #m @(nat_ind_succ … m) -m //
51 lemma tr_xap_push (f) (l):
54 <tr_xap_unfold <tr_xap_unfold
58 lemma tr_xap_pushs_le (f) (n) (m):
59 m ≤ n → m = (⫯*[n]f)@❨m❩.
61 <tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
62 /2 width=1 by nlt_succ_dx/
65 lemma tr_xap_plus (n1) (n2) (f):
66 (⇂*[n2]f)@❨n1❩+f@❨n2❩ = f@❨n1+n2❩.
67 * [| #n1 ] // * [| #n2 ] // #f
68 <nrplus_inj_sn <nrplus_inj_dx
69 <nrplus_inj_sn <nrplus_inj_dx
73 theorem tr_xap_eq_repl (i):
74 stream_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
76 <tr_xap_unfold <tr_xap_unfold
77 /3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/
80 lemma tr_nap_plus_dx_xap (f) (m) (n):
81 ⇂*[↑n]f@❨m❩+f@§❨n❩ = f@§❨m+n❩.
82 /2 width=1 by tr_nap_eq_repl/
85 lemma tr_nap_plus_sn_xap (f) (m) (n):
86 ⇂*[n]f@§❨m❩+f@❨n❩ = f@§❨m+n❩.
89 lemma tr_xap_pos (f) (n):
90 n = ↑↓n → f@❨n❩=↑↓(f@❨n❩).
92 <tr_xap_ninj <nsucc_pnpred //