update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_depth.ma

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 88952c2bc0b4b4edcd60a53c291f1c85a7a4866c..a769327f65b218f655530102b435ca614b60eb22 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -13,16 +13,17 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path.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 ***********************************************************)
 
-rec definition depth (p) on p: pnat ≝
+rec definition depth (p) on p: nat ≝
 match p with
-[ list_empty     â\87\92 ð\9d\9f\8f
+[ list_empty     â\87\92 ð\9d\9f\8e
 | list_lcons l q ⇒
   match l with
-  [ label_d _ ⇒ depth q
+  [ label_d k ⇒ depth q
   | label_m   ⇒ depth q
   | label_L   ⇒ ↑(depth q)
   | label_A   ⇒ depth q
@@ -32,24 +33,65 @@ match p with
 
 interpretation
   "depth (path)"
-  'VerticalBars p = (depth p).
+  'Flat p = (depth p).
 
 (* Basic constructions ******************************************************)
 
-lemma depth_empty: ð\9d\9f\8f = â\9d\98ð\9d\90\9eâ\9d\98.
+lemma depth_empty: ð\9d\9f\8e = â\99­ð\9d\90\9e.
 // qed.
 
-lemma depth_d (q) (n): ❘q❘ = ❘𝗱n◗q❘.
+lemma depth_d_dx (p) (k):
+      ♭p = ♭(p◖𝗱k).
 // qed.
 
-lemma depth_m (q): ❘q❘ = ❘𝗺◗q❘.
+lemma depth_m_dx (p):
+      ♭p = ♭(p◖𝗺).
 // qed.
 
-lemma depth_L (q): ↑❘q❘ = ❘𝗟◗q❘.
+lemma depth_L_dx (p):
+      ↑♭p = ♭(p◖𝗟).
 // qed.
 
-lemma depth_A (q): ❘q❘ = ❘𝗔◗q❘.
+lemma depth_A_dx (p):
+      ♭p = ♭(p◖𝗔).
 // qed.
 
-lemma depth_S (q): ❘q❘ = ❘𝗦◗q❘.
+lemma depth_S_dx (p):
+      ♭p = ♭(p◖𝗦).
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem depth_append (p) (q):
+        (♭p)+(♭q) = ♭(p●q).
+#p #q elim q -q //
+* [ #k ] #q #IH <list_append_lcons_sn
+[ <depth_d_dx <depth_d_dx //
+| <depth_m_dx <depth_m_dx //
+| <depth_L_dx <depth_L_dx //
+| <depth_A_dx <depth_A_dx //
+| <depth_S_dx <depth_S_dx //
+]
+qed.
+
+(* Constructions with path_lcons ********************************************)
+
+lemma depth_d_sn (p) (k):
+      ♭p = ♭(𝗱k◗p).
+// qed.
+
+lemma depth_m_sn (p):
+      ♭p = ♭(𝗺◗p).
+// qed.
+
+lemma depth_L_sn (p):
+      ↑♭p = ♭(𝗟◗p).
+// qed.
+
+lemma depth_A_sn (p):
+      ♭p = ♭(𝗔◗p).
+// qed.
+
+lemma depth_S_sn (p):
+      ♭p = ♭(𝗦◗p).
 // qed.