---

Step * 1 2 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
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)))} 
BY
{ (MemTypeCD
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜bs_tree_max(tr;d)⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

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)
            \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)))
\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:
(MemTypeCD
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}bs\_tree\_max(tr;d)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index