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 "delayed_updating/substitution/lift_length.ma".
16 include "delayed_updating/notation/functions/black_righttriangle_1.ma".
17 include "ground/relocation/tr_uni.ma".
18 include "ground/relocation/tr_compose.ma".
20 (* BASIC UNWIND FOR RELOCATION MAP ******************************************)
22 rec definition unwind1_rmap_pnat (n) (p) on n ā
30 [ label_d n ā (unwind1_rmap_pnat m (ā[š®āØnā©]q))ā(ā[q]š®āØnā©)
31 | label_m ā unwind1_rmap_pnat m q
32 | label_L ā unwind1_rmap_pnat m q
33 | label_A ā unwind1_rmap_pnat m q
34 | label_S ā unwind1_rmap_pnat m q
39 definition unwind1_rmap (p) ā
40 unwind1_rmap_pnat (āāpā) p.
43 "basic unwind (relocation map)"
44 'BlackRightTriangle p = (unwind1_rmap p).
46 (* Basic constructions ******************************************************)
48 lemma unwind1_rmap_unfold (p):
49 unwind1_rmap_pnat (āāpā) p = ā¶p.
52 lemma unwind1_rmap_empty:
56 lemma unwind1_rmap_d_sn (p) (n:pnat):
57 (ā¶(ā[š®āØnā©]p))ā(ā[p]š®āØnā©) = ā¶(š±nāp).
59 <unwind1_rmap_unfold <lift_path_length //
62 lemma unwind1_rmap_m_sn (p):
66 lemma unwind1_rmap_L_sn (p):
70 lemma unwind1_rmap_A_sn (p):
74 lemma unwind1_rmap_S_sn (p):