[ list_empty β π
| list_lcons l q β
match l with
- [ label_node_d n β structure q
- | label_edge_L β πβstructure q
- | label_edge_A β πβstructure q
- | label_edge_S β π¦βstructure q
+ [ label_d n β structure q
+ | label_m β structure q
+ | label_L β πβstructure q
+ | label_A β πβstructure q
+ | label_S β π¦βstructure q
]
].
βp = β(π±nβp).
// qed.
+lemma structure_m_sn (p):
+ βp = β(πΊβp).
+// qed.
+
lemma structure_L_sn (p):
- πββp = β(πβp).
+ (πββp) = β(πβp).
// qed.
lemma structure_A_sn (p):
- πββp = β(πβp).
+ (πββp) = β(πβp).
// qed.
lemma structure_S_sn (p):
- π¦ββp = β(π¦βp).
+ (π¦ββp) = β(π¦βp).
// qed.
(* Main constructions *******************************************************)
#p #n <structure_append //
qed.
+lemma structure_m_dx (p):
+ βp = β(pβπΊ).
+#p <structure_append //
+qed.
+
lemma structure_L_dx (p):
(βp)βπ = β(pβπ).
#p <structure_append //