---

Step * 1 1 of Lemma bs_tree_delete_wf


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index