---

Step * of Lemma member-bs_tree_delete-implies

∀[E:Type]. ∀cmp:comparison(E). ∀x:E. ∀tr:bs_tree(E). ∀z:E.  (z ∈ bs_tree_delete(cmp;x;tr) ⇒ z ∈ tr)
BY
{ (RepeatFor 3 (Intro) THEN (BLemma `bs_tree-induction` THENA Auto)) }

1
1. [E] : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀z:E. (z ∈ bs_tree_delete(cmp;x;bst_null()) ⇒ z ∈ bst_null())

2
1. [E] : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀value,z:E.  (z ∈ bs_tree_delete(cmp;x;bst_leaf(value)) ⇒ z ∈ bst_leaf(value))

3
1. [E] : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).
    ((∀z:E. (z ∈ bs_tree_delete(cmp;x;left) ⇒ z ∈ left))
    ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;right) ⇒ z ∈ right))
    ⇒ (∀z:E. (z ∈ bs_tree_delete(cmp;x;bst_node(left;value;right)) ⇒ z ∈ bst_node(left;value;right))))

---

Latex:

---

Latex:
\mforall{}[E:Type].  \mforall{}cmp:comparison(E).  \mforall{}x:E.  \mforall{}tr:bs\_tree(E).  \mforall{}z:E.    (z  \mmember{}  bs\_tree\_delete(cmp;x;tr)  {}\mRightarrow{}  z  \mmember{}  tr)


By

---

Latex:
(RepeatFor  3  (Intro)  THEN  (BLemma  `bs\_tree-induction`  THENA  Auto))

---

Home Index