X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_depth.ma;h=474bbcbda501f43dd5de91697dd321d58ca33c7f;hb=a4cacf8e269910184348a037106551dbc8a46fd4;hp=efeaf86b40fb7087219bef1d55b705fd4c0c8ce0;hpb=f83215ca9b8d0019c85a991ec90c6c658c0aaff8;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..474bbcbda 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path.ma".
-include "ground/arith/nat_succ.ma".
-include "ground/notation/functions/verticalbars_1.ma".
+include "delayed_updating/notation/functions/flat_1.ma".
+include "ground/arith/nat_plus.ma".
 
 (* DEPTH FOR PATH ***********************************************************)
 
@@ -23,30 +23,70 @@ 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
+  [ label_d _ ⇒ depth q
+  | label_m   ⇒ depth q
+  | label_L   ⇒ ↑(depth q)
+  | label_A   ⇒ depth q
+  | label_S   ⇒ depth q
   ]
 ].
 
 interpretation
   "depth (path)"
-  'VerticalBars p = (depth p).
+  'Flat p = (depth p).
 
 (* Basic constructions ******************************************************)
 
-lemma depth_empty: 𝟎 = ❘𝐞❘.
+lemma depth_empty: 𝟎 = ♭𝐞.
 // qed.
 
-lemma depth_d (q) (n): ❘q❘ = ❘𝗱n◗q❘.
+lemma depth_d_sn (q) (n): ♭q = ♭(𝗱n◗q).
 // qed.
 
-lemma depth_L (q): ↑❘q❘ = ❘𝗟◗q❘.
+lemma depth_m_sn (q): ♭q = ♭(𝗺◗q).
 // qed.
 
-lemma depth_A (q): ❘q❘ = ❘𝗔◗q❘.
+lemma depth_L_sn (q): ↑♭q = ♭(𝗟◗q).
 // qed.
 
-lemma depth_S (q): ❘q❘ = ❘𝗦◗q❘.
+lemma depth_A_sn (q): ♭q = ♭(𝗔◗q).
+// qed.
+
+lemma depth_S_sn (q): ♭q = ♭(𝗦◗q).
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem depth_append (p1) (p2):
+        (♭p2)+(♭p1) = ♭(p1●p2).
+#p1 elim p1 -p1 //
+* [ #n ] #p1 #IH #p2 <list_append_lcons_sn
+[ <depth_d_sn <depth_d_sn //
+| <depth_m_sn <depth_m_sn //
+| <depth_L_sn <depth_L_sn //
+| <depth_A_sn <depth_A_sn //
+| <depth_S_sn <depth_S_sn //
+]
+qed.
+
+(* Constructions with list_rcons ********************************************)
+
+lemma depth_d_dx (p) (n):
+      ♭p = ♭(p◖𝗱n).
+// qed.
+
+lemma depth_m_dx (p):
+      ♭p = ♭(p◖𝗺).
+// qed.
+
+lemma depth_L_dx (p):
+      ↑♭p = ♭(p◖𝗟).
+// qed.
+
+lemma depth_A_dx (p):
+      ♭p = ♭(p◖𝗔).
+// qed.
+
+lemma depth_S_dx (p):
+      ♭p = ♭(p◖𝗦).
 // qed.