---

Step * 2 1 of Lemma bs_tree_insert_wf


1. E : Type
2. cmp : comparison(E)
3. x : E
4. value : E
5. ¬0 < cmp value x
6. bs_tree_ordered(E;cmp;bst_leaf(value))
7. cmp value x < 0
8. True
9. True
10. ∀x@0:E. (False ⇒ 0 < cmp x@0 x)
11. x@0 : E
12. value = x@0 ∈ E
⊢ 0 < cmp x x@0
BY
{ ((RevHypSubst' (-1) 0 THENA Auto) THEN RWO "comparison-anti" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  E  :  Type
2.  cmp  :  comparison(E)
3.  x  :  E
4.  value  :  E
5.  \mneg{}0  <  cmp  value  x
6.  bs\_tree\_ordered(E;cmp;bst\_leaf(value))
7.  cmp  value  x  <  0
8.  True
9.  True
10.  \mforall{}x@0:E.  (False  {}\mRightarrow{}  0  <  cmp  x@0  x)
11.  x@0  :  E
12.  value  =  x@0
\mvdash{}  0  <  cmp  x  x@0


By

---

Latex:
((RevHypSubst'  (-1)  0  THENA  Auto)  THEN  RWO  "comparison-anti"  0  THEN  Auto)

---

Home Index