[ list_empty ⇒ 𝟎
| list_lcons l q ⇒
match l with
- [ label_d _ ⇒ depth q
- | label_m ⇒ depth q
- | label_L ⇒ ↑(depth q)
- | label_A ⇒ depth q
- | label_S ⇒ depth q
+ [ label_d k ⇒ depth q
+ | label_d2 k 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_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_d2_dx (p) (k) (d):
+ ♭p = ♭(p◖𝗱❨k,d❩).
// qed.
-lemma depth_L_sn (q): ↑♭q = ♭(𝗟◗q).
+lemma depth_m_dx (p):
+ ♭p = ♭(p◖𝗺).
+// qed.
+
+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.
(* 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 //
+theorem depth_append (p) (q):
+ (♭p)+(♭q) = ♭(p●q).
+#p #q elim q -q //
+* [ #k | #k #d ] #q #IH <list_append_lcons_sn
+[ <depth_d_dx <depth_d_dx //
+| <depth_d2_dx <depth_d2_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 list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
-lemma depth_d_dx (p) (n):
- ♭p = ♭(p◖𝗱n).
+lemma depth_d_sn (p) (k):
+ ♭p = ♭(𝗱k◗p).
// qed.
-lemma depth_m_dx (p):
- ♭p = ♭(p◖𝗺).
+lemma depth_d2_sn (p) (k) (d):
+ ♭p = ♭(𝗱❨k,d❩◗p).
// qed.
-lemma depth_L_dx (p):
- â\86\91â\99p = â\99(pâ\97\96ð\9d\97\9f).
+lemma depth_m_sn (p):
+ â\99p = â\99(ð\9d\97ºâ\97\97p).
// qed.
-lemma depth_A_dx (p):
- â\99p = â\99(pâ\97\96ð\9d\97\94).
+lemma depth_L_sn (p):
+ â\86\91â\99p = â\99(ð\9d\97\9fâ\97\97p).
// qed.
-lemma depth_S_dx (p):
- ♭p = ♭(p◖𝗦).
+lemma depth_A_sn (p):
+ ♭p = ♭(𝗔◗p).
+// qed.
+
+lemma depth_S_sn (p):
+ ♭p = ♭(𝗦◗p).
// qed.