[ list_empty ⇒ 𝟎
| list_lcons l q ⇒
match l with
- [ 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
+ [ label_d k ⇒ depth q
+ | label_m ⇒ depth q
+ | label_L ⇒ ↑(depth q)
+ | label_A ⇒ depth q
+ | label_S ⇒ depth q
]
].
♭p = ♭(p◖𝗱k).
// qed.
-lemma depth_d2_dx (p) (k) (d):
- ♭p = ♭(p◖𝗱❨k,d❩).
-// qed.
-
lemma depth_m_dx (p):
♭p = ♭(p◖𝗺).
// qed.
theorem depth_append (p) (q):
(♭p)+(♭q) = ♭(p●q).
#p #q elim q -q //
-* [ #k | #k #d ] #q #IH <list_append_lcons_sn
+* [ #k ] #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 //
♭p = ♭(𝗱k◗p).
// qed.
-lemma depth_d2_sn (p) (k) (d):
- ♭p = ♭(𝗱❨k,d❩◗p).
-// qed.
-
lemma depth_m_sn (p):
♭p = ♭(𝗺◗p).
// qed.