(**************************************************************************)
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 ***********************************************************)
[ 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: รฐ\9d\9f\8e = รข\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_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.