---

Step * 1 2 of Lemma bs_tree_delete_wf


1. E : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀value:E. (bs_tree_ordered(E;cmp;bst_leaf(value)) ⇒ bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;bst_leaf(value))))
BY
{ (RepUR ``bs_tree_delete bs_tree_ordered`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  E  :  Type
2.  cmp  :  comparison(E)
3.  x  :  E
\mvdash{}  \mforall{}value:E
        (bs\_tree\_ordered(E;cmp;bst\_leaf(value))
        {}\mRightarrow{}  bs\_tree\_ordered(E;cmp;bs\_tree\_delete(cmp;x;bst\_leaf(value))))


By

---

Latex:
(RepUR  ``bs\_tree\_delete  bs\_tree\_ordered``  0  THEN  Auto)

---

Home Index