1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/arith/pnat_plus.ma".
16 include "ground/relocation/tr_map.ma".
17 include "delayed_updating/notation/functions/verticalbarat_2.ma".
19 (* POSITIVE APPLICATION FOR STACKS OF BASIC RELOCATION MAPS *****************)
21 rec definition sbr_pap (i: pnat) on i: tr_map → pnat.
25 [ lapply (sbr_pap i f) -sbr_pap -i -f
33 "functional positive application (stack of relocation maps)"
34 'VerticalBarAt f i = (sbr_pap i f).
36 (* Basic constructions ******************************************************)
38 lemma sbr_pap_unfold_unit (f):
42 lemma sbr_pap_unfold_unit_succ (f):
43 ∀i. ↑(f❘@❨i❩) = (𝟏⨮f)❘@❨↑i❩.
46 lemma sbr_pap_unfold_succ_bi (f):
47 ∀p,i. i+↑p = (↑p⨮f)❘@❨↑i❩.