X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_depth.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_depth.ma;h=88952c2bc0b4b4edcd60a53c291f1c85a7a4866c;hb=13584a37bbcde10e03c8a488f5b93e1e042da0a6;hp=efeaf86b40fb7087219bef1d55b705fd4c0c8ce0;hpb=2cc4eb5d0210be58286e028278852122dcb68052;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
index efeaf86b4..88952c2bc 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -13,20 +13,20 @@
 (**************************************************************************)
 
 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 ≝
+rec definition depth (p) on p: pnat ≝
 match p with
-[ list_empty     ⇒ 𝟎
+[ 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
   ]
 ].
 
@@ -36,12 +36,15 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma depth_empty: 𝟎 = ❘𝐞❘.
+lemma depth_empty: 𝟏 = ❘𝐞❘.
 // qed.
 
 lemma depth_d (q) (n): ❘q❘ = ❘𝗱n◗q❘.
 // qed.
 
+lemma depth_m (q): ❘q❘ = ❘𝗺◗q❘.
+// qed.
+
 lemma depth_L (q): ↑❘q❘ = ❘𝗟◗q❘.
 // qed.