(**************************************************************************)
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 ***********************************************************)
lemma depth_empty: š = āšā.
// qed.
-lemma depth_d (q) (n): āqā = āš±nāqā.
+lemma depth_d_sn (q) (n): āqā = āš±nāqā.
// qed.
-lemma depth_m (q): āqā = āšŗāqā.
+lemma depth_m_sn (q): āqā = āšŗāqā.
// qed.
-lemma depth_L (q): āāqā = āšāqā.
+lemma depth_L_sn (q): āāqā = āšāqā.
// qed.
-lemma depth_A (q): āqā = āšāqā.
+lemma depth_A_sn (q): āqā = āšāqā.
// qed.
-lemma depth_S (q): āqā = āš¦āqā.
+lemma depth_S_sn (q): āqā = āš¦āqā.
// qed.
+
+(* Advanced constructions with nplus ****************************************)
+
+lemma depth_plus (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.