---

Step * of Lemma member-bs_tree_max

∀[E:Type]
  ∀tr:bs_tree(E). ∀d,z:E.
    ((z ∈ snd(bs_tree_max(tr;d)) ∨ (z = (fst(bs_tree_max(tr;d))) ∈ E)) ⇒ (z ∈ tr ∨ ((↑bst_null?(tr)) ∧ (z = d ∈ E))))
BY
{ (Intro THEN (BLemma `bs_tree-induction` THENA Auto)) }

1
1. [E] : Type
⊢ ∀d,z:E.
    ((z ∈ snd(bs_tree_max(bst_null();d)) ∨ (z = (fst(bs_tree_max(bst_null();d))) ∈ E))
    ⇒ (z ∈ bst_null() ∨ ((↑bst_null?(bst_null())) ∧ (z = d ∈ E))))

2
1. [E] : Type
⊢ ∀value,d,z:E.
    ((z ∈ snd(bs_tree_max(bst_leaf(value);d)) ∨ (z = (fst(bs_tree_max(bst_leaf(value);d))) ∈ E))
    ⇒ (z ∈ bst_leaf(value) ∨ ((↑bst_null?(bst_leaf(value))) ∧ (z = d ∈ E))))

3
1. [E] : Type
⊢ ∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).
    ((∀d,z:E.
        ((z ∈ snd(bs_tree_max(left;d)) ∨ (z = (fst(bs_tree_max(left;d))) ∈ E))
        ⇒ (z ∈ left ∨ ((↑bst_null?(left)) ∧ (z = d ∈ E)))))
    ⇒ (∀d,z:E.
          ((z ∈ snd(bs_tree_max(right;d)) ∨ (z = (fst(bs_tree_max(right;d))) ∈ E))
          ⇒ (z ∈ right ∨ ((↑bst_null?(right)) ∧ (z = d ∈ E)))))
    ⇒ (∀d,z:E.
          ((z ∈ snd(bs_tree_max(bst_node(left;value;right);d))
          ∨ (z = (fst(bs_tree_max(bst_node(left;value;right);d))) ∈ E))
          ⇒ (z ∈ bst_node(left;value;right) ∨ ((↑bst_null?(bst_node(left;value;right))) ∧ (z = d ∈ E))))))

---

Latex:

---

Latex:
\mforall{}[E:Type]
    \mforall{}tr:bs\_tree(E).  \mforall{}d,z:E.
        ((z  \mmember{}  snd(bs\_tree\_max(tr;d))  \mvee{}  (z  =  (fst(bs\_tree\_max(tr;d)))))
        {}\mRightarrow{}  (z  \mmember{}  tr  \mvee{}  ((\muparrow{}bst\_null?(tr))  \mwedge{}  (z  =  d))))


By

---

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

---

Home Index