(* STRUCTURE FOR PATH *******************************************************)
-rec definition path_structure (p) on p β
+rec definition structure (p) on p β
match p with
[ list_empty β π
| list_lcons l q β
match l with
- [ label_node_d n β path_structure q
- | label_edge_L β πβpath_structure q
- | label_edge_A β πβpath_structure q
- | label_edge_S β π¦βpath_structure q
+ [ label_d k β structure q
+ | label_m β structure q
+ | label_L β (structure q)βπ
+ | label_A β (structure q)βπ
+ | label_S β (structure q)βπ¦
]
].
interpretation
"structure (path)"
- 'CircledTimes p = (path_structure p).
+ 'CircledTimes p = (structure p).
+
+(* Basic constructions ******************************************************)
+
+lemma structure_empty:
+ π = βπ.
+// qed.
+
+lemma structure_d_dx (p) (k):
+ βp = β(pβπ±k).
+// qed.
+
+lemma structure_m_dx (p):
+ βp = β(pβπΊ).
+// qed.
+
+lemma structure_L_dx (p):
+ (βp)βπ = β(pβπ).
+// qed.
+
+lemma structure_A_dx (p):
+ (βp)βπ = β(pβπ).
+// qed.
+
+lemma structure_S_dx (p):
+ (βp)βπ¦ = β(pβπ¦).
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem structure_idem (p):
+ βp = ββp.
+#p elim p -p [| * [ #k ] #p #IH ] //
+qed.
+
+theorem structure_append (p) (q):
+ βpββq = β(pβq).
+#p #q elim q -q [| * [ #k ] #q #IH ]
+[||*: <list_append_lcons_sn ] //
+qed.
+
+(* Constructions with path_lcons ********************************************)
+
+lemma structure_d_sn (p) (k):
+ βp = β(π±kβp).
+#p #n <structure_append //
+qed.
+
+lemma structure_m_sn (p):
+ βp = β(πΊβp).
+#p <structure_append //
+qed.
+
+lemma structure_L_sn (p):
+ (πββp) = β(πβp).
+#p <structure_append //
+qed.
+
+lemma structure_A_sn (p):
+ (πββp) = β(πβp).
+#p <structure_append //
+qed.
+
+lemma structure_S_sn (p):
+ (π¦ββp) = β(π¦βp).
+#p <structure_append //
+qed.