---

Step * of Lemma bs_tree_max_wf

∀[E:Type]. ∀[cmp:comparison(E)]. ∀[tr:ordered_bs_tree(E;cmp)]. ∀[d:E].
  (bs_tree_max(tr;d) ∈ {p:E × ordered_bs_tree(E;cmp)| 
                        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
{ (Auto THEN D -2 THEN Unfold `ordered_bs_tree` 0) }

1
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)))} 

---

Latex:

---

Latex:
\mforall{}[E:Type].  \mforall{}[cmp:comparison(E)].  \mforall{}[tr:ordered\_bs\_tree(E;cmp)].  \mforall{}[d:E].
    (bs\_tree\_max(tr;d)  \mmember{}  \{p:E  \mtimes{}  ordered\_bs\_tree(E;cmp)| 
                                                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:
(Auto  THEN  D  -2  THEN  Unfold  `ordered\_bs\_tree`  0)

---

Home Index