---

Step * 3 2 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,z:E.
     ((z ∈ snd(bs_tree_max(right;d)) ∨ (z = (fst(bs_tree_max(right;d))) ∈ E)) ⇒ (z ∈ right ∨ (False ∧ (z = d ∈ E))))
8. d : E
9. z : 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
{ ((D -3 With ⌜d⌝  THENA Auto) THEN (D -1 With ⌜z⌝  THENA Auto)) }

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. (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)))

---

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.  \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{}  (False  \mwedge{}  (z  =  d))))
8.  d  :  E
9.  z  :  E
\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:
((D  -3  With  \mkleeneopen{}d\mkleeneclose{}    THENA  Auto)  THEN  (D  -1  With  \mkleeneopen{}z\mkleeneclose{}    THENA  Auto))

---

Home Index