---

Step * 1 of Lemma bs_tree_max_wf


1. E : Type
2. cmp : comparison(E)
3. tr : bs_tree(E)
4. bs_tree_ordered(E;cmp;tr)
5. d : E
⊢ bs_tree_max(tr;d) ∈ {p:E × {tr:bs_tree(E)| bs_tree_ordered(E;cmp;tr)} | 
                       let m,t = p 
                       in (∀x:E. (x ∈ tr ⇒ (x ∈ t ∨ (x = m ∈ E))))
                          ∧ ((¬↑bst_null?(tr)) ⇒ m ∈ tr)
                          ∧ (∀x:E. (x ∈ t ⇒ (x ∈ tr ∧ 0 < cmp x m)))} 
BY
{ Assert ⌜let m,t = bs_tree_max(tr;d) 
          in bs_tree_ordered(E;cmp;t)
             ∧ (∀x:E. (x ∈ tr ⇒ (x ∈ t ∨ (x = m ∈ E))))
             ∧ ((¬↑bst_null?(tr)) ⇒ m ∈ tr)
             ∧ (∀x:E. (x ∈ t ⇒ (x ∈ tr ∧ 0 < cmp x m)))⌝⋅ }

1
.....assertion..... 
1. E : Type
2. cmp : comparison(E)
3. tr : bs_tree(E)
4. bs_tree_ordered(E;cmp;tr)
5. d : E
⊢ let m,t = bs_tree_max(tr;d) 
  in bs_tree_ordered(E;cmp;t)
     ∧ (∀x:E. (x ∈ tr ⇒ (x ∈ t ∨ (x = m ∈ E))))
     ∧ ((¬↑bst_null?(tr)) ⇒ m ∈ tr)
     ∧ (∀x:E. (x ∈ t ⇒ (x ∈ tr ∧ 0 < cmp x m)))

2
1. E : Type
2. cmp : comparison(E)
3. tr : bs_tree(E)
4. bs_tree_ordered(E;cmp;tr)
5. d : E
6. let m,t = bs_tree_max(tr;d) 
   in bs_tree_ordered(E;cmp;t)
      ∧ (∀x:E. (x ∈ tr ⇒ (x ∈ t ∨ (x = m ∈ E))))
      ∧ ((¬↑bst_null?(tr)) ⇒ m ∈ tr)
      ∧ (∀x:E. (x ∈ t ⇒ (x ∈ tr ∧ 0 < cmp x m)))
⊢ bs_tree_max(tr;d) ∈ {p:E × {tr:bs_tree(E)| bs_tree_ordered(E;cmp;tr)} | 
                       let m,t = p 
                       in (∀x:E. (x ∈ tr ⇒ (x ∈ t ∨ (x = m ∈ E))))
                          ∧ ((¬↑bst_null?(tr)) ⇒ m ∈ tr)
                          ∧ (∀x:E. (x ∈ t ⇒ (x ∈ tr ∧ 0 < cmp x m)))} 

---

Latex:

---

Latex:

1.  E  :  Type
2.  cmp  :  comparison(E)
3.  tr  :  bs\_tree(E)
4.  bs\_tree\_ordered(E;cmp;tr)
5.  d  :  E
\mvdash{}  bs\_tree\_max(tr;d)  \mmember{}  \{p:E  \mtimes{}  \{tr:bs\_tree(E)|  bs\_tree\_ordered(E;cmp;tr)\}  | 
                                              let  m,t  =  p 
                                              in  (\mforall{}x:E.  (x  \mmember{}  tr  {}\mRightarrow{}  (x  \mmember{}  t  \mvee{}  (x  =  m))))
                                                    \mwedge{}  ((\mneg{}\muparrow{}bst\_null?(tr))  {}\mRightarrow{}  m  \mmember{}  tr)
                                                    \mwedge{}  (\mforall{}x:E.  (x  \mmember{}  t  {}\mRightarrow{}  (x  \mmember{}  tr  \mwedge{}  0  <  cmp  x  m)))\} 


By

---

Latex:
Assert  \mkleeneopen{}let  m,t  =  bs\_tree\_max(tr;d) 
                in  bs\_tree\_ordered(E;cmp;t)
                      \mwedge{}  (\mforall{}x:E.  (x  \mmember{}  tr  {}\mRightarrow{}  (x  \mmember{}  t  \mvee{}  (x  =  m))))
                      \mwedge{}  ((\mneg{}\muparrow{}bst\_null?(tr))  {}\mRightarrow{}  m  \mmember{}  tr)
                      \mwedge{}  (\mforall{}x:E.  (x  \mmember{}  t  {}\mRightarrow{}  (x  \mmember{}  tr  \mwedge{}  0  <  cmp  x  m)))\mkleeneclose{}\mcdot{}

---

Home Index