---

Step * 3 of Lemma member-bs_tree_max


1. [E] : Type
⊢ ∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).
    ((∀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)))))
    ⇒ (∀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)))))
    ⇒ (∀d,z:E.
          ((z ∈ snd(bs_tree_max(bst_node(left;value;right);d))
          ∨ (z = (fst(bs_tree_max(bst_node(left;value;right);d))) ∈ E))
          ⇒ (z ∈ bst_node(left;value;right) ∨ ((↑bst_null?(bst_node(left;value;right))) ∧ (z = d ∈ E))))))
BY
{ (RepeatFor 7 (Intro) THEN RepUR ``bs_tree_max`` 0 THEN Fold `bs_tree_max` 0 THEN AutoSplit) }

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

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

---

Latex:

---

Latex:

1.  [E]  :  Type
\mvdash{}  \mforall{}left:bs\_tree(E).  \mforall{}value:E.  \mforall{}right:bs\_tree(E).
        ((\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)))))
        {}\mRightarrow{}  (\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)))))
        {}\mRightarrow{}  (\mforall{}d,z:E.
                    ((z  \mmember{}  snd(bs\_tree\_max(bst\_node(left;value;right);d))
                    \mvee{}  (z  =  (fst(bs\_tree\_max(bst\_node(left;value;right);d)))))
                    {}\mRightarrow{}  (z  \mmember{}  bst\_node(left;value;right)
                          \mvee{}  ((\muparrow{}bst\_null?(bst\_node(left;value;right)))  \mwedge{}  (z  =  d))))))


By

---

Latex:
(RepeatFor  7  (Intro)  THEN  RepUR  ``bs\_tree\_max``  0  THEN  Fold  `bs\_tree\_max`  0  THEN  AutoSplit)

---

Home Index