---

Step * 1 of Lemma member-bs_tree_max


1. [E] : Type
⊢ ∀d,z:E.
    ((z ∈ snd(bs_tree_max(bst_null();d)) ∨ (z = (fst(bs_tree_max(bst_null();d))) ∈ E))
    ⇒ (z ∈ bst_null() ∨ ((↑bst_null?(bst_null())) ∧ (z = d ∈ E))))
BY
{ (RepUR ``bs_tree_max member_bs_tree`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [E]  :  Type
\mvdash{}  \mforall{}d,z:E.
        ((z  \mmember{}  snd(bs\_tree\_max(bst\_null();d))  \mvee{}  (z  =  (fst(bs\_tree\_max(bst\_null();d)))))
        {}\mRightarrow{}  (z  \mmember{}  bst\_null()  \mvee{}  ((\muparrow{}bst\_null?(bst\_null()))  \mwedge{}  (z  =  d))))


By

---

Latex:
(RepUR  ``bs\_tree\_max  member\_bs\_tree``  0  THEN  Auto)

---

Home Index