---

Step * 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)
⊢ bs_tree_lookup(cmp;x;tr) ∈ (∃z:E [(((cmp z x) = 0 ∈ ℤ) ∧ z ∈ tr)]) ∨ (↓∀z:E. (z ∈ tr ⇒ (¬((cmp z x) = 0 ∈ ℤ))))
BY
{ Assert ⌜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 ∈ ℤ)))⌝⋅ }

1
.....assertion..... 
1. E : Type
2. cmp : comparison(E)
3. x : E
4. tr : bs_tree(E)
5. bs_tree_ordered(E;cmp;tr)
⊢ 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 ∈ ℤ)))

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

---

Latex:

---

Latex:

1.  E  :  Type
2.  cmp  :  comparison(E)
3.  x  :  E
4.  tr  :  bs\_tree(E)
5.  bs\_tree\_ordered(E;cmp;tr)
\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:
Assert  \mkleeneopen{}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)))\mkleeneclose{}\mcdot{}

---

Home Index