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/circled_times_1.ma".
18 (* STRUCTURE FOR PATH *******************************************************)
20 rec definition structure (p) on p β
25 [ label_node_d n β structure q
26 | label_edge_L β πβstructure q
27 | label_edge_A β πβstructure q
28 | label_edge_S β π¦βstructure q
34 'CircledTimes p = (structure p).
36 (* Basic constructions ******************************************************)
38 lemma structure_empty:
42 lemma structure_d_sn (p) (n):
43 βp = β(π±β¨nβ©βp).
46 lemma structure_L_sn (p):
47 πββp = β(πβp).
50 lemma structure_A_sn (p):
51 πββp = β(πβp).
54 lemma structure_S_sn (p):
55 π¦ββp = β(π¦βp).
58 (* Main constructions *******************************************************)
60 theorem structure_idem (p):
62 #p elim p -p [| * [ #n ] #p #IH ] //
65 theorem structure_append (p1) (p2):
66 βp1ββp2 = β(p1βp2).
67 #p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
68 [||*: <list_append_lcons_sn ] //
71 (* Constructions with list_rcons ********************************************)
73 lemma structure_d_dx (p) (n):
74 βp = β(pβπ±β¨nβ©).
75 #p #n <structure_append //
78 lemma structure_L_dx (p):
79 (βp)βπ = β(pβπ).
80 #p <structure_append //
83 lemma structure_A_dx (p):
84 (βp)βπ = β(pβπ).
85 #p <structure_append //
88 lemma structure_S_dx (p):
89 (βp)βπ¦ = β(pβπ¦).
90 #p <structure_append //