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_d n β structure q
26 | label_m β structure q
27 | label_L β πβstructure q
28 | label_A β πβstructure q
29 | label_S β π¦βstructure q
35 'CircledTimes p = (structure p).
37 (* Basic constructions ******************************************************)
39 lemma structure_empty:
43 lemma structure_d_sn (p) (n):
44 βp = β(π±nβp).
47 lemma structure_m_sn (p):
51 lemma structure_L_sn (p):
52 (πββp) = β(πβp).
55 lemma structure_A_sn (p):
56 (πββp) = β(πβp).
59 lemma structure_S_sn (p):
60 (π¦ββp) = β(π¦βp).
63 (* Main constructions *******************************************************)
65 theorem structure_idem (p):
67 #p elim p -p [| * [ #n ] #p #IH ] //
70 theorem structure_append (p1) (p2):
71 βp1ββp2 = β(p1βp2).
72 #p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
73 [||*: <list_append_lcons_sn ] //
76 (* Constructions with list_rcons ********************************************)
78 lemma structure_d_dx (p) (n):
79 βp = β(pβπ±n).
80 #p #n <structure_append //
83 lemma structure_m_dx (p):
85 #p <structure_append //
88 lemma structure_L_dx (p):
89 (βp)βπ = β(pβπ).
90 #p <structure_append //
93 lemma structure_A_dx (p):
94 (βp)βπ = β(pβπ).
95 #p <structure_append //
98 lemma structure_S_dx (p):
99 (βp)βπ¦ = β(pβπ¦).
100 #p <structure_append //