---

Step * 1 2 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. case bs_tree_lookup(cmp;x;tr)
 of inl(z) =>
 ((cmp z x) = 0 ∈ ℤ) ∧ z ∈ tr
 | inr(_) =>
 ∀z:E. (z ∈ tr ⇒ (¬((cmp z x) = 0 ∈ ℤ)))
⊢ bs_tree_lookup(cmp;x;tr) ∈ (∃z:E [(((cmp z x) = 0 ∈ ℤ) ∧ z ∈ tr)]) ∨ (↓∀z:E. (z ∈ tr ⇒ (¬((cmp z x) = 0 ∈ ℤ))))
BY
{ (MoveToConcl (-1) THEN (GenConclTerm⌜bs_tree_lookup(cmp;x;tr)⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto) }

1
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 ∈ ℤ)))

---

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.  case  bs\_tree\_lookup(cmp;x;tr)
  of  inl(z)  =>
  ((cmp  z  x)  =  0)  \mwedge{}  z  \mmember{}  tr
  |  inr($_{}$)  =>
  \mforall{}z:E.  (z  \mmember{}  tr  {}\mRightarrow{}  (\mneg{}((cmp  z  x)  =  0)))
\mvdash{}  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:
(MoveToConcl  (-1)
  THEN  (GenConclTerm\mkleeneopen{}bs\_tree\_lookup(cmp;x;tr)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index