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 k ⇒ 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_dx (p) (k):
47 lemma structure_m_dx (p):
51 lemma structure_L_dx (p):
55 lemma structure_A_dx (p):
59 lemma structure_S_dx (p):
63 (* Main constructions *******************************************************)
65 theorem structure_idem (p):
67 #p elim p -p [| * [ #k ] #p #IH ] //
70 theorem structure_append (p) (q):
72 #p #q elim q -q [| * [ #k ] #q #IH ]
73 [||*: <list_append_lcons_sn ] //
76 (* Constructions with path_lcons ********************************************)
78 lemma structure_d_sn (p) (k):
80 #p #n <structure_append //
83 lemma structure_m_sn (p):
85 #p <structure_append //
88 lemma structure_L_sn (p):
90 #p <structure_append //
93 lemma structure_A_sn (p):
95 #p <structure_append //
98 lemma structure_S_sn (p):
100 #p <structure_append //