---

Step * 3 2 1 1 of Lemma member-bs_tree_max


1. [E] : Type
2. left : bs_tree(E)
3. value : E
4. right : bs_tree(E)
5. ¬↑bst_null?(right)
6. ∀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))))
7. d : E
8. z : E
9. v1 : E
10. v2 : bs_tree(E)
⊢ ((z ∈ v2 ∨ (z = v1 ∈ E)) ⇒ (z ∈ right ∨ (False ∧ (z = d ∈ E))))
⇒ (z ∈ bst_node(left;value;v2) ∨ (z = v1 ∈ E))
⇒ (z ∈ bst_node(left;value;right) ∨ (False ∧ (z = d ∈ E)))
BY
{ (RepUR ``member_bs_tree`` 0
   THEN Fold `member_bs_tree` 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN (D -2 THENA Auto)
   THEN SplitOrHyps
   THEN Auto) }

---

Latex:

---

Latex:

1.  [E]  :  Type
2.  left  :  bs\_tree(E)
3.  value  :  E
4.  right  :  bs\_tree(E)
5.  \mneg{}\muparrow{}bst\_null?(right)
6.  \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))))
7.  d  :  E
8.  z  :  E
9.  v1  :  E
10.  v2  :  bs\_tree(E)
\mvdash{}  ((z  \mmember{}  v2  \mvee{}  (z  =  v1))  {}\mRightarrow{}  (z  \mmember{}  right  \mvee{}  (False  \mwedge{}  (z  =  d))))
{}\mRightarrow{}  (z  \mmember{}  bst\_node(left;value;v2)  \mvee{}  (z  =  v1))
{}\mRightarrow{}  (z  \mmember{}  bst\_node(left;value;right)  \mvee{}  (False  \mwedge{}  (z  =  d)))


By

---

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

---

Home Index