(**************************************************************************)
include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/flat_1.ma".
include "ground/arith/nat_plus.ma".
-include "ground/notation/functions/verticalbars_1.ma".
(* DEPTH FOR PATH ***********************************************************)
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_sn (q) (n): ❘q❘ = ❘𝗱n◗q❘.
+lemma depth_d_dx (p) (k):
+ ♭p = ♭(p◖𝗱k).
// qed.
-lemma depth_m_sn (q): ❘q❘ = ❘𝗺◗q❘.
+lemma depth_m_dx (p):
+ ♭p = ♭(p◖𝗺).
// qed.
-lemma depth_L_sn (q): ↑❘q❘ = ❘𝗟◗q❘.
+lemma depth_L_dx (p):
+ ↑♭p = ♭(p◖𝗟).
// qed.
-lemma depth_A_sn (q): ❘q❘ = ❘𝗔◗q❘.
+lemma depth_A_dx (p):
+ ♭p = ♭(p◖𝗔).
// qed.
-lemma depth_S_sn (q): ❘q❘ = ❘𝗦◗q❘.
+lemma depth_S_dx (p):
+ ♭p = ♭(p◖𝗦).
// 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 //
+(* 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.