---

Step * 3 of Lemma member-bs_tree_delete


1. [E] : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).
    ((bs_tree_ordered(E;cmp;left) ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;left) ⇐⇒ z ∈ left ∧ (¬((cmp z x) = 0 ∈ ℤ)))))
    ⇒ (bs_tree_ordered(E;cmp;right)
       ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;right) ⇐⇒ z ∈ right ∧ (¬((cmp z x) = 0 ∈ ℤ)))))
    ⇒ bs_tree_ordered(E;cmp;bst_node(left;value;right))
    ⇒ (∀z:E
          (z ∈ bs_tree_delete(cmp;x;bst_node(left;value;right))
          ⇐⇒ z ∈ bst_node(left;value;right) ∧ (¬((cmp z x) = 0 ∈ ℤ)))))
BY
{ RepeatFor 7 (Intro) }

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. bs_tree_ordered(E;cmp;left) ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;left) ⇐⇒ z ∈ left ∧ (¬((cmp z x) = 0 ∈ ℤ))))
8. bs_tree_ordered(E;cmp;right) ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;right) ⇐⇒ z ∈ right ∧ (¬((cmp z x) = 0 ∈ ℤ))))
9. bs_tree_ordered(E;cmp;bst_node(left;value;right))
10. z : E
⊢ z ∈ bs_tree_delete(cmp;x;bst_node(left;value;right)) ⇐⇒ z ∈ bst_node(left;value;right) ∧ (¬((cmp z x) = 0 ∈ ℤ))

---

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).
        ((bs\_tree\_ordered(E;cmp;left)
          {}\mRightarrow{}  (\mforall{}z:E.  (z  \mmember{}  bs\_tree\_delete(cmp;x;left)  \mLeftarrow{}{}\mRightarrow{}  z  \mmember{}  left  \mwedge{}  (\mneg{}((cmp  z  x)  =  0)))))
        {}\mRightarrow{}  (bs\_tree\_ordered(E;cmp;right)
              {}\mRightarrow{}  (\mforall{}z:E.  (z  \mmember{}  bs\_tree\_delete(cmp;x;right)  \mLeftarrow{}{}\mRightarrow{}  z  \mmember{}  right  \mwedge{}  (\mneg{}((cmp  z  x)  =  0)))))
        {}\mRightarrow{}  bs\_tree\_ordered(E;cmp;bst\_node(left;value;right))
        {}\mRightarrow{}  (\mforall{}z:E
                    (z  \mmember{}  bs\_tree\_delete(cmp;x;bst\_node(left;value;right))
                    \mLeftarrow{}{}\mRightarrow{}  z  \mmember{}  bst\_node(left;value;right)  \mwedge{}  (\mneg{}((cmp  z  x)  =  0)))))


By

---

Latex:
RepeatFor  7  (Intro)

---

Home Index