(**************************************************************************)
include "delayed_updating/syntax/path.ma".
-include "ground/arith/nat_succ.ma".
+include "ground/arith/nat_plus.ma".
include "ground/notation/functions/verticalbars_1.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
]
].
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.