---

Step * 2 of Lemma member_bs_tree_insert


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 ∈ ℤ))))))
BY
{ (Intros
   THEN RepUR ``bs_tree_insert`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Repeat (AutoSplit)
   THEN (RepUR ``member_bs_tree`` 0 THEN Auto)
   THEN SplitOrHyps
   THEN Auto
   THEN Try (((OrRight THEN Auto) THEN (HypSubst' (-1) (-3) THEN Auto) THEN RWO "comparison-anti" (-3) THEN Auto))) }

1
1. E : Type
2. cmp : comparison(E)
3. x : E
4. value : E
5. ¬cmp value x < 0
6. ¬0 < cmp value x
7. bs_tree_ordered(E;cmp;bst_leaf(value))
8. y : E
9. value = y ∈ E
10. ¬((cmp x y) = 0 ∈ ℤ)
⊢ x = y ∈ E

---

Latex:

---

Latex:

1.  [E]  :  Type
2.  cmp  :  comparison(E)
3.  x  :  E
\mvdash{}  \mforall{}value:E
        (bs\_tree\_ordered(E;cmp;bst\_leaf(value))
        {}\mRightarrow{}  (\mforall{}y:E
                    (y  \mmember{}  bs\_tree\_insert(cmp;x;bst\_leaf(value))
                    \mLeftarrow{}{}\mRightarrow{}  (y  =  x)  \mvee{}  (y  \mmember{}  bst\_leaf(value)  \mwedge{}  (\mneg{}((cmp  x  y)  =  0))))))


By

---

Latex:
(Intros
  THEN  RepUR  ``bs\_tree\_insert``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Repeat  (AutoSplit)
  THEN  (RepUR  ``member\_bs\_tree``  0  THEN  Auto)
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Try  (((OrRight  THEN  Auto)
                        THEN  (HypSubst'  (-1)  (-3)  THEN  Auto)
                        THEN  RWO  "comparison-anti"  (-3)
                        THEN  Auto)))

---

Home Index