---

Step * of Lemma member-bs_tree_delete

∀[E:Type]
  ∀cmp:comparison(E). ∀x:E. ∀tr:ordered_bs_tree(E;cmp). ∀z:E.
    (z ∈ bs_tree_delete(cmp;x;tr) ⇐⇒ z ∈ tr ∧ (¬((cmp z x) = 0 ∈ ℤ)))
BY
{ (RepeatFor 4 (Intro)
   THEN D -1
   THEN (Assert bs_tree_ordered(E;cmp;tr) BY
               (Unhide THEN Auto))
   THEN Thin (-2)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (BLemma `bs_tree-induction` THENA Auto)) }

1
1. [E] : Type
2. cmp : comparison(E)
3. x : E
⊢ bs_tree_ordered(E;cmp;bst_null())
⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;bst_null()) ⇐⇒ z ∈ bst_null() ∧ (¬((cmp z x) = 0 ∈ ℤ))))

2
1. [E] : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀value:E
    (bs_tree_ordered(E;cmp;bst_leaf(value))
    ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;bst_leaf(value)) ⇐⇒ z ∈ bst_leaf(value) ∧ (¬((cmp z x) = 0 ∈ ℤ)))))

3
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) ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;left) ⇐⇒ z ∈ left ∧ (¬((cmp z x) = 0 ∈ ℤ)))))
    ⇒ (bs_tree_ordered(E;cmp;right)
       ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;right) ⇐⇒ z ∈ right ∧ (¬((cmp z x) = 0 ∈ ℤ)))))
    ⇒ bs_tree_ordered(E;cmp;bst_node(left;value;right))
    ⇒ (∀z:E
          (z ∈ bs_tree_delete(cmp;x;bst_node(left;value;right))
          ⇐⇒ z ∈ bst_node(left;value;right) ∧ (¬((cmp z x) = 0 ∈ ℤ)))))

---

Latex:

---

Latex:
\mforall{}[E:Type]
    \mforall{}cmp:comparison(E).  \mforall{}x:E.  \mforall{}tr:ordered\_bs\_tree(E;cmp).  \mforall{}z:E.
        (z  \mmember{}  bs\_tree\_delete(cmp;x;tr)  \mLeftarrow{}{}\mRightarrow{}  z  \mmember{}  tr  \mwedge{}  (\mneg{}((cmp  z  x)  =  0)))


By

---

Latex:
(RepeatFor  4  (Intro)
  THEN  D  -1
  THEN  (Assert  bs\_tree\_ordered(E;cmp;tr)  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  (-2)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (BLemma  `bs\_tree-induction`  THENA  Auto))

---

Home Index