1 include "ground/relocation/tr_uni_pap.ma".
2 include "ground/relocation/tr_compose_pap.ma".
3 include "ground/relocation/tr_pap_eq.ma".
4 include "ground/relocation/tr_pap_hdtl_eq.ma".
5 include "ground/notation/functions/atsection_2.ma".
6 include "ground/arith/nat_lt.ma".
7 include "ground/arith/nat_plus_pplus.ma".
8 include "ground/arith/nat_pred_succ.ma".
10 lemma nlt_npsucc_bi (n1) (n2):
11 n1 < n2 → npsucc n1 < npsucc n2.
12 #n1 #n2 #Hn elim Hn -n2 //
13 #n2 #_ #IH /2 width=1 by plt_succ_dx_trans/
16 definition tr_nap (f) (l:nat): nat ≝
20 "functional non-negative application (total relocation maps)"
21 'AtSection f l = (tr_nap f l).
23 lemma tr_nap_unfold (f) (l):
27 lemma tr_pap_succ_nap (f) (l):
31 lemma tr_compose_nap (f2) (f1) (l):
32 f2@§❨f1@§❨l❩❩ = (f2∘f1)@§❨l❩.
34 <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
35 <tr_compose_pap <npsucc_pred //
38 lemma tr_uni_nap (n) (m):
42 <tr_uni_pap <nrplus_npsucc_sn //
45 lemma tr_nap_push (f):
46 ∀l. ↑(f@§❨l❩) = (⫯f)@§❨↑l❩.
48 <tr_nap_unfold <tr_nap_unfold
49 <tr_pap_push <pnpred_psucc //
52 lemma tr_nap_pushs_lt (f) (n) (m):
53 m < n → m = (⫯*[n]f)@§❨m❩.
55 <tr_nap_unfold <tr_pap_pushs_le
56 /2 width=1 by nlt_npsucc_bi/
59 theorem tr_nap_eq_repl (i):
60 stream_eq_repl … (λf1,f2. f1@§❨i❩ = f2@§❨i❩).
62 <tr_nap_unfold <tr_nap_unfold
63 /3 width=1 by tr_pap_eq_repl, eq_f/
66 lemma tr_eq_inv_nap_zero_tl_bi (f1) (f2):
67 f1@§❨𝟎❩ = f2@§❨𝟎❩ → ⇂f1 ≗ ⇂f2 → f1 ≗ f2.
69 <tr_nap_unfold <tr_nap_unfold #H1 #H2
70 /3 width=1 by tr_eq_inv_pap_unit_tl_bi, eq_inv_pnpred_bi/
73 lemma tr_nap_plus_sn (f) (m) (n):
74 (⫯⇂*[↑n]f)@§❨m❩+f@§❨n❩ = f@§❨m+n❩.
75 #f #m @(nat_ind_succ … m) -m [| #m #_ ] #n
76 [ <nplus_zero_sn <nplus_zero_sn //
77 | <tr_nap_push <nplus_comm in ⊢ (???%);
78 <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
79 <nsucc_pnpred <nrplus_inj_sn <nrplus_pnpred_dx
80 >nrplus_npsucc_sn <nrplus_inj_dx
81 <pplus_comm in ⊢ (???%); <tr_pap_plus //
85 lemma tr_nap_plus_dx (f) (m) (n):
86 ⇂*[n]f@§❨m❩+(⫯f)@§❨n❩ = f@§❨m+n❩.
87 #f #m #n @(nat_ind_succ … n) -n [| #n #_ ]
90 <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
91 <nsucc_pnpred <nplus_pnpred_sn
92 >nrplus_npsucc_sn <nrplus_inj_dx