---

Step * 1 1 of Lemma bs_tree_lookup_wf

.....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 ∈ ℤ)))
BY
{ (RepeatFor 2 (MoveToConcl (-1)) THEN (BLemma `bs_tree-induction` THENA Auto)) }

1
1. E : Type
2. cmp : comparison(E)
3. x : E
⊢ bs_tree_ordered(E;cmp;bst_null())
⇒ case bs_tree_lookup(cmp;x;bst_null())
    of inl(z) =>
    ((cmp z x) = 0 ∈ ℤ) ∧ z ∈ bst_null()
    | inr(_) =>
    ∀z:E. (z ∈ bst_null() ⇒ (¬((cmp z x) = 0 ∈ ℤ)))

2
1. E : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀value:E
    (bs_tree_ordered(E;cmp;bst_leaf(value))
    ⇒ case bs_tree_lookup(cmp;x;bst_leaf(value))
        of inl(z) =>
        ((cmp z x) = 0 ∈ ℤ) ∧ z ∈ bst_leaf(value)
        | inr(_) =>
        ∀z:E. (z ∈ bst_leaf(value) ⇒ (¬((cmp z x) = 0 ∈ ℤ))))

3
1. E : Type
2. cmp : comparison(E)
3. x : E
⊢ ∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).
    ((bs_tree_ordered(E;cmp;left)
     ⇒ case bs_tree_lookup(cmp;x;left)
         of inl(z) =>
         ((cmp z x) = 0 ∈ ℤ) ∧ z ∈ left
         | inr(_) =>
         ∀z:E. (z ∈ left ⇒ (¬((cmp z x) = 0 ∈ ℤ))))
    ⇒ (bs_tree_ordered(E;cmp;right)
       ⇒ case bs_tree_lookup(cmp;x;right)
           of inl(z) =>
           ((cmp z x) = 0 ∈ ℤ) ∧ z ∈ right
           | inr(_) =>
           ∀z:E. (z ∈ right ⇒ (¬((cmp z x) = 0 ∈ ℤ))))
    ⇒ bs_tree_ordered(E;cmp;bst_node(left;value;right))
    ⇒ case bs_tree_lookup(cmp;x;bst_node(left;value;right))
        of inl(z) =>
        ((cmp z x) = 0 ∈ ℤ) ∧ z ∈ bst_node(left;value;right)
        | inr(_) =>
        ∀z:E. (z ∈ bst_node(left;value;right) ⇒ (¬((cmp z x) = 0 ∈ ℤ))))

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))  THEN  (BLemma  `bs\_tree-induction`  THENA  Auto))

---

Home Index