---

Step * of Lemma bs_tree_lookup_wf

∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:ordered_bs_tree(E;cmp)].
  (bs_tree_lookup(cmp;x;tr) ∈ (∃z:E [(((cmp z x) = 0 ∈ ℤ) ∧ z ∈ tr)]) ∨ (↓∀z:E. (z ∈ tr ⇒ (¬((cmp z x) = 0 ∈ ℤ)))))
BY
{ (Auto THEN D -1) }

1
1. E : Type
2. cmp : comparison(E)
3. x : E
4. tr : bs_tree(E)
5. bs_tree_ordered(E;cmp;tr)
⊢ bs_tree_lookup(cmp;x;tr) ∈ (∃z:E [(((cmp z x) = 0 ∈ ℤ) ∧ z ∈ tr)]) ∨ (↓∀z:E. (z ∈ tr ⇒ (¬((cmp z x) = 0 ∈ ℤ))))

---

Latex:

---

Latex:
\mforall{}[E:Type].  \mforall{}[cmp:comparison(E)].  \mforall{}[x:E].  \mforall{}[tr:ordered\_bs\_tree(E;cmp)].
    (bs\_tree\_lookup(cmp;x;tr)  \mmember{}  (\mexists{}z:E  [(((cmp  z  x)  =  0)  \mwedge{}  z  \mmember{}  tr)])
      \mvee{}  (\mdownarrow{}\mforall{}z:E.  (z  \mmember{}  tr  {}\mRightarrow{}  (\mneg{}((cmp  z  x)  =  0)))))


By

---

Latex:
(Auto  THEN  D  -1)

---

Home Index