---

Step * 1 2 1 1 1 1 of Lemma aa_max_ltree_spec2


1. t : aa_ltree()@i
2. val : @i
3. left_subtree : aa_ltree()@i
4. right_subtree : aa_ltree()@i
5. j:
     ((aa_binary_search_tree(left_subtree)  (aa_max_ltree(left_subtree) = (inl j )))
      aa_bst_member_prop(j;left_subtree))@i
6. j:
     ((aa_binary_search_tree(right_subtree)  (aa_max_ltree(right_subtree) = (inl j )))
      aa_bst_member_prop(j;right_subtree))@i
7. j : @i
8. aa_binary_search_tree(left_subtree)@i
9. aa_binary_search_tree(right_subtree)@i
10. case aa_max_ltree(left_subtree) of inl(maxl) => maxl < val | inr(ul) => 0  0@i
11. case aa_min_ltree(right_subtree) of inl(minr) => val < minr | inr(ur) => 0  0@i
12. x : 
13. aa_max_ltree(right_subtree) = (inl x )
14. (inl imax(val;x) ) = (inl j )@i
15. x = j
16. val  x
17. aa_bst_member_prop(j;right_subtree)
 (val = j)  ((j < val)  aa_bst_member_prop(j;left_subtree))  ((val < j)  aa_bst_member_prop(j;right_subtree))
BY
{ BoolCase (val = x) THEN Auto' }

1
1. t : aa_ltree()@i
2. val : @i
3. left_subtree : aa_ltree()@i
4. right_subtree : aa_ltree()@i
5. j:
     ((aa_binary_search_tree(left_subtree)  (aa_max_ltree(left_subtree) = (inl j )))
      aa_bst_member_prop(j;left_subtree))@i
6. j:
     ((aa_binary_search_tree(right_subtree)  (aa_max_ltree(right_subtree) = (inl j )))
      aa_bst_member_prop(j;right_subtree))@i
7. j : @i
8. aa_binary_search_tree(left_subtree)@i
9. aa_binary_search_tree(right_subtree)@i
10. case aa_max_ltree(left_subtree) of inl(maxl) => maxl < val | inr(ul) => 0  0@i
11. case aa_min_ltree(right_subtree) of inl(minr) => val < minr | inr(ur) => 0  0@i
12. x : 
13. aa_max_ltree(right_subtree) = (inl x )
14. (inl imax(val;x) ) = (inl j )@i
15. x = j
16. val  x
17. aa_bst_member_prop(j;right_subtree)
18. (val = x)
 (val = j)  ((j < val)  aa_bst_member_prop(j;left_subtree))  ((val < j)  aa_bst_member_prop(j;right_subtree))



1.  t  :  aa\_ltree(\mBbbZ{})@i
2.  val  :  \mBbbZ{}@i
3.  left$_{subtree}$  :  aa\_ltree(\mBbbZ{})@i
4.  right$_{subtree}$  :  aa\_ltree(\mBbbZ{})@i
5.  \mforall{}j:\mBbbZ{}
          ((aa\_binary\_search\_tree(left$_{subtree}$)  \mwedge{}  (aa\_max\_ltree(left$_\mbackslash{}ff\000C7bsubtree}$)  =  (inl  j  )))
          {}\mRightarrow{}  aa\_bst\_member\_prop(j;left$_{subtree}$))@i
6.  \mforall{}j:\mBbbZ{}
          ((aa\_binary\_search\_tree(right$_{subtree}$)  \mwedge{}  (aa\_max\_ltree(right$_\mbackslash{}\000Cff7bsubtree}$)  =  (inl  j  )))
          {}\mRightarrow{}  aa\_bst\_member\_prop(j;right$_{subtree}$))@i
7.  j  :  \mBbbZ{}@i
8.  aa\_binary\_search\_tree(left$_{subtree}$)@i
9.  aa\_binary\_search\_tree(right$_{subtree}$)@i
10.  case  aa\_max\_ltree(left$_{subtree}$)  of  inl(maxl)  =>  maxl  <  val  |  inr(ul)  =>  \000C0  \mleq{}  0@i
11.  case  aa\_min\_ltree(right$_{subtree}$)  of  inl(minr)  =>  val  <  minr  |  inr(ur)  =>\000C  0  \mleq{}  0@i
12.  x  :  \mBbbZ{}
13.  aa\_max\_ltree(right$_{subtree}$)  =  (inl  x  )
14.  (inl  imax(val;x)  )  =  (inl  j  )@i
15.  x  =  j
16.  val  \mleq{}  x
17.  aa\_bst\_member\_prop(j;right$_{subtree}$)
\mvdash{}  (val  =  j)
\mvee{}  ((j  <  val)  \mwedge{}  aa\_bst\_member\_prop(j;left$_{subtree}$))
\mvee{}  ((val  <  j)  \mwedge{}  aa\_bst\_member\_prop(j;right$_{subtree}$))


By

BoolCase  \mkleeneopen{}(val  =\msubz{}  x)\mkleeneclose{}  THEN  Auto'\mcdot{}



Home Index