---

Step * 2 1 of Lemma member-bs_tree_delete


1. E : Type
2. value : E
3. cmp : comparison(E)
4. x : E
5. bs_tree_ordered(E;cmp;bst_leaf(value))
6. z : E
7. (cmp x value) = 0 ∈ ℤ
8. value = z ∈ E
9. ¬((cmp value x) = 0 ∈ ℤ)
⊢ False
BY
{ (D -1 THEN RWO "comparison-anti" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  E  :  Type
2.  value  :  E
3.  cmp  :  comparison(E)
4.  x  :  E
5.  bs\_tree\_ordered(E;cmp;bst\_leaf(value))
6.  z  :  E
7.  (cmp  x  value)  =  0
8.  value  =  z
9.  \mneg{}((cmp  value  x)  =  0)
\mvdash{}  False


By

---

Latex:
(D  -1  THEN  RWO  "comparison-anti"  0  THEN  Auto)

---

Home Index