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/syntax/path.ma".
16 include "delayed_updating/notation/functions/black_righttriangle_2.ma".
17 include "delayed_updating/notation/functions/black_righttriangle_1.ma".
18 include "ground/relocation/tr_uni.ma".
19 include "ground/relocation/tr_compose.ma".
21 (* UNWIND MAP FOR PATH ******************************************************)
23 rec definition unwind2_rmap (f) (p) on p: tr_map ≝
28 [ label_d n ⇒ (unwind2_rmap f q)∘𝐮❨n❩
29 | label_m ⇒ unwind2_rmap f q
30 | label_L ⇒ ⫯(unwind2_rmap f q)
31 | label_A ⇒ unwind2_rmap f q
32 | label_S ⇒ unwind2_rmap f q
37 "tailed unwind map (reversed path)"
38 'BlackRightTriangle f p = (unwind2_rmap f p).
41 "unwind map (reversed path)"
42 'BlackRightTriangle p = (unwind2_rmap tr_id p).
44 (* Basic constructions ******************************************************)
46 lemma unwind2_rmap_empty (f):
50 lemma unwind2_rmap_d_sn (f) (p) (n:pnat):
51 (▶[f]p∘𝐮❨n❩) = ▶[f](𝗱n◗p).
54 lemma unwind2_rmap_m_sn (f) (p):
58 lemma unwind2_rmap_L_sn (f) (p):
62 lemma unwind2_rmap_A_sn (f) (p):
66 lemma unwind2_rmap_S_sn (f) (p):
70 (* Constructions with list_append *******************************************)
72 lemma unwind2_rmap_append (f) (p1) (p2):
73 ▶[▶[f]p2]p1 = ▶[f](p1●p2).
75 * [ #n ] #p1 #IH #p2 //
76 [ <unwind2_rmap_m_sn <unwind2_rmap_m_sn //
77 | <unwind2_rmap_L_sn <unwind2_rmap_L_sn //
78 | <unwind2_rmap_A_sn <unwind2_rmap_A_sn //
79 | <unwind2_rmap_S_sn <unwind2_rmap_S_sn //
83 (* Constructions with list_rcons ********************************************)
85 lemma unwind2_rmap_d_dx (f) (p) (n:pnat):
86 ▶[f∘𝐮❨n❩]p = ▶[f](p◖𝗱n).
89 lemma unwind2_rmap_m_dx (f) (p):
93 lemma unwind2_rmap_L_dx (f) (p):
97 lemma unwind2_rmap_A_dx (f) (p):
101 lemma unwind2_rmap_S_dx (f) (p):