1 (**) (* reverse include *)
2 include "ground/arith/nat_rplus_pplus.ma".
3 include "ground/relocation/tr_pn_eq.ma".
4 include "ground/relocation/tr_compose_pn.ma".
5 include "ground/relocation/nap.ma".
6 include "ground/notation/functions/at_2.ma".
8 definition tr_xap (f) (l:nat): nat ≝
12 "functional extended application (total relocation maps)"
13 'At f l = (tr_xap f l).
15 lemma tr_xap_unfold (f) (l):
19 lemma tr_xap_zero (f):
23 lemma tr_xap_ninj (f) (p):
24 ninj (f@⧣❨p❩) = f@❨ninj p❩.
27 lemma tr_xap_succ_nap (f) (n):
33 lemma tr_compose_xap (f2) (f1) (l):
34 f2@❨f1@❨l❩❩ = (f2∘f1)@❨l❩.
36 <tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
37 >tr_compose_nap >tr_compose_push_bi //
40 lemma tr_uni_xap_succ (n) (m):
44 <tr_nap_push <tr_uni_nap //
47 lemma tr_uni_xap (n) (m):
49 #n #m @(nat_ind_succ … m) -m //
52 lemma tr_xap_push (f) (l):
55 <tr_xap_unfold <tr_xap_unfold
59 lemma tr_xap_pushs_le (f) (n) (m):
60 m ≤ n → m = (⫯*[n]f)@❨m❩.
62 <tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
63 /2 width=1 by nlt_succ_dx/
66 lemma tr_xap_plus (n1) (n2) (f):
67 (⇂*[n2]f)@❨n1❩+f@❨n2❩ = f@❨n1+n2❩.
68 * [| #n1 ] // * [| #n2 ] // #f
69 <nrplus_inj_sn <nrplus_inj_dx
70 <nrplus_inj_sn <nrplus_inj_dx
74 theorem tr_xap_eq_repl (i):
75 stream_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
77 <tr_xap_unfold <tr_xap_unfold
78 /3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/
81 lemma tr_nap_plus (f) (m) (n):
82 ⇂*[↑n]f@❨m❩+f@§❨n❩ = f@§❨m+n❩.
83 /2 width=1 by eq_inv_nsucc_bi/
86 lemma tr_xap_pos (f) (n):
87 n = ↑↓n → f@❨n❩=↑↓(f@❨n❩).
89 <tr_xap_ninj <nsucc_pnpred //