---

Step * 2 of Lemma member-bs_tree_max


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index