+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "delayed_updating/syntax/path.ma".
+include "ground/arith/nat_succ.ma".
+include "ground/notation/functions/verticalbars_1.ma".
+
+(* DEPTH FOR PATH ***********************************************************)
+
+rec definition depth (p) on p: nat โ
+match p with
+[ 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
+ ]
+].
+
+interpretation
+ "depth (path)"
+ 'VerticalBars p = (depth p).
+
+(* Basic constructions ******************************************************)
+
+lemma depth_empty: ๐ = โ๐โ.
+// qed.
+
+lemma depth_d (q) (n): โqโ = โ๐ฑโจnโฉโqโ.
+// qed.
+
+lemma depth_L (q): โโqโ = โ๐โqโ.
+// qed.
+
+lemma depth_A (q): โqโ = โ๐โqโ.
+// qed.
+
+lemma depth_S (q): โqโ = โ๐ฆโqโ.
+// qed.