---

Step * 2 2 of Lemma member-bs_tree_delete


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index