[ list_empty ā š
| list_lcons l q ā
match l with
- [ label_node_d _ ā depth q
- | label_edge_L ā ā(depth q)
- | label_edge_A ā depth q
- | label_edge_S ā depth q
+ [ label_d _ ā depth q
+ | label_m ā depth q
+ | label_L ā ā(depth q)
+ | label_A ā depth q
+ | label_S ā depth q
]
].
lemma depth_empty: š = āšā.
// qed.
-lemma depth_d (q) (n): āqā = āš±āØnā©āqā.
+lemma depth_d (q) (n): āqā = āš±nāqā.
+// qed.
+
+lemma depth_m (q): āqā = āšŗāqā.
// qed.
lemma depth_L (q): āāqā = āšāqā.