---

Step * 3 1 of Lemma member-bs_tree_max


1. [E] : Type
2. left : bs_tree(E)
3. value : E
4. right : bs_tree(E)
5. ∀d,z:E.
     ((z ∈ snd(bs_tree_max(left;d)) ∨ (z = (fst(bs_tree_max(left;d))) ∈ E))
     ⇒ (z ∈ left ∨ ((↑bst_null?(left)) ∧ (z = d ∈ E))))
6. ∀d,z:E.
     ((z ∈ snd(bs_tree_max(right;d)) ∨ (z = (fst(bs_tree_max(right;d))) ∈ E))
     ⇒ (z ∈ right ∨ ((↑bst_null?(right)) ∧ (z = d ∈ E))))
7. d : E
8. z : E
9. ↑bst_null?(right)
⊢ (z ∈ left ∨ (z = value ∈ E)) ⇒ (z ∈ bst_node(left;value;right) ∨ (False ∧ (z = d ∈ E)))
BY
{ (Auto THEN RepUR ``member_bs_tree`` 0 THEN Fold `member_bs_tree` 0 THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  [E]  :  Type
2.  left  :  bs\_tree(E)
3.  value  :  E
4.  right  :  bs\_tree(E)
5.  \mforall{}d,z:E.
          ((z  \mmember{}  snd(bs\_tree\_max(left;d))  \mvee{}  (z  =  (fst(bs\_tree\_max(left;d)))))
          {}\mRightarrow{}  (z  \mmember{}  left  \mvee{}  ((\muparrow{}bst\_null?(left))  \mwedge{}  (z  =  d))))
6.  \mforall{}d,z:E.
          ((z  \mmember{}  snd(bs\_tree\_max(right;d))  \mvee{}  (z  =  (fst(bs\_tree\_max(right;d)))))
          {}\mRightarrow{}  (z  \mmember{}  right  \mvee{}  ((\muparrow{}bst\_null?(right))  \mwedge{}  (z  =  d))))
7.  d  :  E
8.  z  :  E
9.  \muparrow{}bst\_null?(right)
\mvdash{}  (z  \mmember{}  left  \mvee{}  (z  =  value))  {}\mRightarrow{}  (z  \mmember{}  bst\_node(left;value;right)  \mvee{}  (False  \mwedge{}  (z  =  d)))


By

---

Latex:
(Auto  THEN  RepUR  ``member\_bs\_tree``  0  THEN  Fold  `member\_bs\_tree`  0  THEN  D  -1  THEN  Auto)

---

Home Index