---

Step * 3 2 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. (z ∈ snd(bs_tree_max(right;d)) ∨ (z = (fst(bs_tree_max(right;d))) ∈ E)) ⇒ (z ∈ right ∨ (False ∧ (z = d ∈ E)))
⊢ (z ∈ snd(let m,b' = bs_tree_max(right;d) 
           in <m, bst_node(left;value;b')>)
∨ (z = (fst(let m,b' = bs_tree_max(right;d) in <m, bst_node(left;value;b')>)) ∈ E))
⇒ (z ∈ bst_node(left;value;right) ∨ (False ∧ (z = d ∈ E)))
BY
{ (MoveToConcl (-1) THEN (GenConclTerm bs_tree_max(right;d)⋅ THENA Auto) THEN Thin (-1) THEN D -1 THEN Reduce 0) }

1
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)))

---

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.  (z  \mmember{}  snd(bs\_tree\_max(right;d))  \mvee{}  (z  =  (fst(bs\_tree\_max(right;d)))))
{}\mRightarrow{}  (z  \mmember{}  right  \mvee{}  (False  \mwedge{}  (z  =  d)))
\mvdash{}  (z  \mmember{}  snd(let  m,b'  =  bs\_tree\_max(right;d) 
                      in  <m,  bst\_node(left;value;b')>)
\mvee{}  (z  =  (fst(let  m,b'  =  bs\_tree\_max(right;d)  in  <m,  bst\_node(left;value;b')>))))
{}\mRightarrow{}  (z  \mmember{}  bst\_node(left;value;right)  \mvee{}  (False  \mwedge{}  (z  =  d)))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConclTerm  bs\_tree\_max(right;d)\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index