]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
921863e5065948b5b73449c61337a28d4c04ea85
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / nap.ma
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/notation/functions/atsection_2.ma".
5 include "ground/arith/nat_lt.ma".
6 include "ground/arith/nat_plus_rplus.ma".
7 include "ground/arith/nat_pred_succ.ma".
8
9 lemma nlt_npsucc_bi (n1) (n2):
10       n1 < n2 → npsucc n1 < npsucc n2.
11 #n1 #n2 #Hn elim Hn -n2 //
12 #n2 #_ #IH /2 width=1 by plt_succ_dx_trans/
13 qed.
14
15 definition tr_nap (f) (l:nat): nat ≝
16            ↓(f@⧣❨↑l❩).
17
18 interpretation
19   "functional non-negative application (total relocation maps)"
20   'AtSection f l = (tr_nap f l).
21
22 lemma tr_nap_unfold (f) (l):
23       ↓(f@⧣❨↑l❩) = f@§❨l❩.
24 // qed.
25
26 lemma tr_pap_succ_nap (f) (l):
27       ↑(f@§❨l❩) = f@⧣❨↑l❩.
28 // qed.
29
30 lemma tr_compose_nap (f2) (f1) (l):
31       f2@§❨f1@§❨l❩❩ = (f2∘f1)@§❨l❩.
32 #f2 #f1 #l
33 <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
34 <tr_compose_pap <npsucc_pred //
35 qed.
36
37 lemma tr_uni_nap (n) (m):
38       m + n = 𝐮❨n❩@§❨m❩.
39 #n #m
40 <tr_nap_unfold
41 <tr_uni_pap <nrplus_npsucc_sn //
42 qed.
43
44 lemma tr_nap_push (f):
45       ∀l. ↑(f@§❨l❩) = (⫯f)@§❨↑l❩.
46 #f #l
47 <tr_nap_unfold <tr_nap_unfold
48 <tr_pap_push <pnpred_psucc //
49 qed.
50
51 lemma tr_nap_pushs_lt (f) (n) (m):
52       m < n → m = (⫯*[n]f)@§❨m❩.
53 #f #n #m #Hmn
54 <tr_nap_unfold <tr_pap_pushs_le
55 /2 width=1 by nlt_npsucc_bi/
56 qed-.
57
58 theorem tr_nap_eq_repl (i):
59         stream_eq_repl … (λf1,f2. f1@§❨i❩ = f2@§❨i❩).
60 #i #f1 #f2 #Hf
61 <tr_nap_unfold <tr_nap_unfold
62 /3 width=1 by tr_pap_eq_repl, eq_f/
63 qed.