---

Step * 3 of Lemma member-bs_tree_delete-implies


1. [E] : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).
    ((∀z:E. (z ∈ bs_tree_delete(cmp;x;left) ⇒ z ∈ left))
    ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;right) ⇒ z ∈ right))
    ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;bst_node(left;value;right)) ⇒ z ∈ bst_node(left;value;right))))
BY
{ (RepeatFor 6 (Intro)
   THEN RepUR ``bs_tree_delete member_bs_tree`` 0
   THEN Fold `bs_tree_delete` 0
   THEN Fold `member_bs_tree` 0
   THEN Repeat (AutoSplit)) }

1
1. [E] : Type
2. cmp : comparison(E)
3. x : E
4. left : bs_tree(E)
5. value : E
6. right : bs_tree(E)
7. ∀z:E. (z ∈ bs_tree_delete(cmp;x;left) ⇒ z ∈ left)
8. ∀z:E. (z ∈ bs_tree_delete(cmp;x;right) ⇒ z ∈ right)
9. z : E
10. 0 < cmp x value
⊢ z ∈ bst_node(bs_tree_delete(cmp;x;left);value;right) ⇒ ((value = z ∈ E) ∨ z ∈ left ∨ z ∈ right)

2
1. [E] : Type
2. cmp : comparison(E)
3. x : E
4. left : bs_tree(E)
5. value : E
6. ¬0 < cmp x value
7. right : bs_tree(E)
8. ∀z:E. (z ∈ bs_tree_delete(cmp;x;left) ⇒ z ∈ left)
9. ∀z:E. (z ∈ bs_tree_delete(cmp;x;right) ⇒ z ∈ right)
10. z : E
11. 0 < cmp value x
⊢ z ∈ bst_node(left;value;bs_tree_delete(cmp;x;right)) ⇒ ((value = z ∈ E) ∨ z ∈ left ∨ z ∈ right)

3
1. [E] : Type
2. cmp : comparison(E)
3. x : E
4. left : bs_tree(E)
5. ¬↑bst_null?(left)
6. value : E
7. ¬0 < cmp value x
8. ¬0 < cmp x value
9. right : bs_tree(E)
10. ∀z:E. (z ∈ bs_tree_delete(cmp;x;left) ⇒ z ∈ left)
11. ∀z:E. (z ∈ bs_tree_delete(cmp;x;right) ⇒ z ∈ right)
12. z : E
⊢ z ∈ let m,a' = bs_tree_max(left;value) in bst_node(a';m;right) ⇒ ((value = z ∈ E) ∨ z ∈ left ∨ z ∈ right)

---

Latex:

---

Latex:

1.  [E]  :  Type
2.  cmp  :  comparison(E)
3.  x  :  E
\mvdash{}  \mforall{}left:bs\_tree(E).  \mforall{}value:E.  \mforall{}right:bs\_tree(E).
        ((\mforall{}z:E.  (z  \mmember{}  bs\_tree\_delete(cmp;x;left)  {}\mRightarrow{}  z  \mmember{}  left))
        {}\mRightarrow{}  (\mforall{}z:E.  (z  \mmember{}  bs\_tree\_delete(cmp;x;right)  {}\mRightarrow{}  z  \mmember{}  right))
        {}\mRightarrow{}  (\mforall{}z:E
                    (z  \mmember{}  bs\_tree\_delete(cmp;x;bst\_node(left;value;right))  {}\mRightarrow{}  z  \mmember{}  bst\_node(left;value;right))))


By

---

Latex:
(RepeatFor  6  (Intro)
  THEN  RepUR  ``bs\_tree\_delete  member\_bs\_tree``  0
  THEN  Fold  `bs\_tree\_delete`  0
  THEN  Fold  `member\_bs\_tree`  0
  THEN  Repeat  (AutoSplit))

---

Home Index