---

Step * 1 2 1 of Lemma bs_tree_lookup_wf


1. E : Type
2. cmp : comparison(E)
3. x : E
4. tr : bs_tree(E)
5. bs_tree_ordered(E;cmp;tr)
6. y : Unit@i
7. bs_tree_lookup(cmp;x;tr) = (inr y ) ∈ (E?)
8. ∀z:E. (z ∈ tr ⇒ (¬((cmp z x) = 0 ∈ ℤ)))
⊢ y ∈ ↓∀z:E. (z ∈ tr ⇒ (¬((cmp z x) = 0 ∈ ℤ)))
BY
{ ((DVar `y' THEN MemTypeCD) THEN Auto) }

---

Latex:

---

Latex:

1.  E  :  Type
2.  cmp  :  comparison(E)
3.  x  :  E
4.  tr  :  bs\_tree(E)
5.  bs\_tree\_ordered(E;cmp;tr)
6.  y  :  Unit@i
7.  bs\_tree\_lookup(cmp;x;tr)  =  (inr  y  )
8.  \mforall{}z:E.  (z  \mmember{}  tr  {}\mRightarrow{}  (\mneg{}((cmp  z  x)  =  0)))
\mvdash{}  y  \mmember{}  \mdownarrow{}\mforall{}z:E.  (z  \mmember{}  tr  {}\mRightarrow{}  (\mneg{}((cmp  z  x)  =  0)))


By

---

Latex:
((DVar  `y'  THEN  MemTypeCD)  THEN  Auto)

---

Home Index