---

Step * 1 3 of Lemma bs_tree_delete_wf


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) ⇒ bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;left)))
    ⇒ (bs_tree_ordered(E;cmp;right) ⇒ bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;right)))
    ⇒ bs_tree_ordered(E;cmp;bst_node(left;value;right))
    ⇒ bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;bst_node(left;value;right))))
BY
{ (Auto
   THEN RepUR ``bs_tree_ordered`` -1
   THEN (Fold `bs_tree_ordered` (-1) THEN ExRepD)
   THEN ThinTrivial
   THEN RepUR ``bs_tree_delete`` 0
   THEN Fold `bs_tree_delete` 0) }

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)
8. bs_tree_ordered(E;cmp;right)
9. ∀x:E. (x ∈ left ⇒ 0 < cmp x value)
10. ∀x:E. (x ∈ right ⇒ 0 < cmp value x)
11. bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;right))
12. bs_tree_ordered(E;cmp;bs_tree_delete(cmp;x;left))
⊢ bs_tree_ordered(E;cmp;if (0) < (cmp x value)
                           then bst_node(bs_tree_delete(cmp;x;left);value;right)
                           else if (0) < (cmp value x)
                                   then bst_node(left;value;bs_tree_delete(cmp;x;right))
                                   else if bst_null?(left)
                                        then right
                                        else let m,a' = bs_tree_max(left;value) 
                                             in bst_node(a';m;right)
                                        fi )

---

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{}  bs\_tree\_ordered(E;cmp;bs\_tree\_delete(cmp;x;left)))
        {}\mRightarrow{}  (bs\_tree\_ordered(E;cmp;right)  {}\mRightarrow{}  bs\_tree\_ordered(E;cmp;bs\_tree\_delete(cmp;x;right)))
        {}\mRightarrow{}  bs\_tree\_ordered(E;cmp;bst\_node(left;value;right))
        {}\mRightarrow{}  bs\_tree\_ordered(E;cmp;bs\_tree\_delete(cmp;x;bst\_node(left;value;right))))


By

---

Latex:
(Auto
  THEN  RepUR  ``bs\_tree\_ordered``  -1
  THEN  (Fold  `bs\_tree\_ordered`  (-1)  THEN  ExRepD)
  THEN  ThinTrivial
  THEN  RepUR  ``bs\_tree\_delete``  0
  THEN  Fold  `bs\_tree\_delete`  0)

---

Home Index