---

Step * of Lemma sq_stable__member_bs_tree

∀[E:Type]. ∀cmp:comparison(E). ∀x:E. ∀tr:ordered_bs_tree(E;cmp).  SqStable(x ∈ tr)
BY
{ (Intros
   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)
   THEN RepUR ``member_bs_tree`` 0
   THEN Try (Fold `member_bs_tree` 0 ⋅)
   THEN Auto) }

1
1. [E] : Type
2. cmp : comparison(E)
3. x : E
4. left : bs_tree(E)
5. value : E
6. right : bs_tree(E)
7. bs_tree_ordered(E;cmp;left) ⇒ SqStable(x ∈ left)
8. bs_tree_ordered(E;cmp;right) ⇒ SqStable(x ∈ right)
9. bs_tree_ordered(E;cmp;bst_node(left;value;right))
⊢ SqStable((value = x ∈ E) ∨ x ∈ left ∨ x ∈ right)

---

Latex:

---

Latex:
\mforall{}[E:Type].  \mforall{}cmp:comparison(E).  \mforall{}x:E.  \mforall{}tr:ordered\_bs\_tree(E;cmp).    SqStable(x  \mmember{}  tr)


By

---

Latex:
(Intros
  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)
  THEN  RepUR  ``member\_bs\_tree``  0
  THEN  Try  (Fold  `member\_bs\_tree`  0  \mcdot{})
  THEN  Auto)

---

Home Index