---

Step * of Lemma member_bs_tree_insert

∀[E:Type]
  ∀cmp:comparison(E). ∀x:E. ∀tr:ordered_bs_tree(E;cmp). ∀y:E.
    (y ∈ bs_tree_insert(cmp;x;tr) ⇐⇒ (y = x ∈ E) ∨ (y ∈ tr ∧ (¬((cmp x y) = 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())
⇒ (∀y:E. (y ∈ bs_tree_insert(cmp;x;bst_null()) ⇐⇒ (y = x ∈ E) ∨ (y ∈ bst_null() ∧ (¬((cmp x y) = 0 ∈ ℤ)))))

2
1. [E] : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀value:E
    (bs_tree_ordered(E;cmp;bst_leaf(value))
    ⇒ (∀y:E
          (y ∈ bs_tree_insert(cmp;x;bst_leaf(value)) ⇐⇒ (y = x ∈ E) ∨ (y ∈ bst_leaf(value) ∧ (¬((cmp x y) = 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)
     ⇒ (∀y:E. (y ∈ bs_tree_insert(cmp;x;left) ⇐⇒ (y = x ∈ E) ∨ (y ∈ left ∧ (¬((cmp x y) = 0 ∈ ℤ))))))
    ⇒ (bs_tree_ordered(E;cmp;right)
       ⇒ (∀y:E. (y ∈ bs_tree_insert(cmp;x;right) ⇐⇒ (y = x ∈ E) ∨ (y ∈ right ∧ (¬((cmp x y) = 0 ∈ ℤ))))))
    ⇒ bs_tree_ordered(E;cmp;bst_node(left;value;right))
    ⇒ (∀y:E
          (y ∈ bs_tree_insert(cmp;x;bst_node(left;value;right))
          ⇐⇒ (y = x ∈ E) ∨ (y ∈ bst_node(left;value;right) ∧ (¬((cmp x y) = 0 ∈ ℤ))))))

---

Latex:

---

Latex:
\mforall{}[E:Type]
    \mforall{}cmp:comparison(E).  \mforall{}x:E.  \mforall{}tr:ordered\_bs\_tree(E;cmp).  \mforall{}y:E.
        (y  \mmember{}  bs\_tree\_insert(cmp;x;tr)  \mLeftarrow{}{}\mRightarrow{}  (y  =  x)  \mvee{}  (y  \mmember{}  tr  \mwedge{}  (\mneg{}((cmp  x  y)  =  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