---

Step * 1 2 1 1 of Lemma aa_max_ltree_spec


1. t : aa_ltree()@i
2. val : @i
3. left_subtree : aa_ltree()@i
4. right_subtree : aa_ltree()@i
5. aa_binary_search_tree(left_subtree)
 (i:. (aa_bst_member_prop(i;left_subtree)  (j:. (((inl j ) = aa_max_ltree(left_subtree))  (i  j)))))@i
6. aa_binary_search_tree(right_subtree)
 (i:. (aa_bst_member_prop(i;right_subtree)  (j:. (((inl j ) = aa_max_ltree(right_subtree))  (i  j)))))@i
7. aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))@i
8. i : @i
9. aa_bst_member_prop(i;aa_lt_node(val;left_subtree;right_subtree))@i
 j:
   (((inl j ) = case aa_max_ltree(right_subtree) of inl(intval2) => inl imax(val;intval2)  | inr(unitval2) => inl val )
    (i  j))
BY
{ InstConcl [case aa_max_ltree(right_subtree) of inl(rmaxint) => imax(val;rmaxint) | inr(unitval) => val] THEN Auto'
 }

1
1. t : aa_ltree()@i
2. val : @i
3. left_subtree : aa_ltree()@i
4. right_subtree : aa_ltree()@i
5. aa_binary_search_tree(left_subtree)
 (i:. (aa_bst_member_prop(i;left_subtree)  (j:. (((inl j ) = aa_max_ltree(left_subtree))  (i  j)))))@i
6. aa_binary_search_tree(right_subtree)
 (i:. (aa_bst_member_prop(i;right_subtree)  (j:. (((inl j ) = aa_max_ltree(right_subtree))  (i  j)))))@i
7. aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))@i
8. i : @i
9. aa_bst_member_prop(i;aa_lt_node(val;left_subtree;right_subtree))@i
 (inl case aa_max_ltree(right_subtree) of inl(rmaxint) => imax(val;rmaxint) | inr(unitval) => val )
= case aa_max_ltree(right_subtree) of inl(intval2) => inl imax(val;intval2)  | inr(unitval2) => inl val 

2
1. t : aa_ltree()@i
2. val : @i
3. left_subtree : aa_ltree()@i
4. right_subtree : aa_ltree()@i
5. aa_binary_search_tree(left_subtree)
 (i:. (aa_bst_member_prop(i;left_subtree)  (j:. (((inl j ) = aa_max_ltree(left_subtree))  (i  j)))))@i
6. aa_binary_search_tree(right_subtree)
 (i:. (aa_bst_member_prop(i;right_subtree)  (j:. (((inl j ) = aa_max_ltree(right_subtree))  (i  j)))))@i
7. aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))@i
8. i : @i
9. aa_bst_member_prop(i;aa_lt_node(val;left_subtree;right_subtree))@i
 i  case aa_max_ltree(right_subtree) of inl(rmaxint) => imax(val;rmaxint) | inr(unitval) => val



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.  aa\_binary\_search\_tree(left$_{subtree}$)
{}\mRightarrow{}  (\mforall{}i:\mBbbZ{}
            (aa\_bst\_member\_prop(i;left$_{subtree}$)
            {}\mRightarrow{}  (\mexists{}j:\mBbbZ{}.  (((inl  j  )  =  aa\_max\_ltree(left$_{subtree}$))  \mwedge{}  (i  \mleq{}  j)))))@i
6.  aa\_binary\_search\_tree(right$_{subtree}$)
{}\mRightarrow{}  (\mforall{}i:\mBbbZ{}
            (aa\_bst\_member\_prop(i;right$_{subtree}$)
            {}\mRightarrow{}  (\mexists{}j:\mBbbZ{}.  (((inl  j  )  =  aa\_max\_ltree(right$_{subtree}$))  \mwedge{}  (i  \mleq{}  j)))))@i
7.  aa\_binary\_search\_tree(aa\_lt\_node(val;left$_{subtree}$;right$_{sub\000Ctree}$))@i
8.  i  :  \mBbbZ{}@i
9.  aa\_bst\_member\_prop(i;aa\_lt\_node(val;left$_{subtree}$;right$_{subt\000Cree}$))@i
\mvdash{}  \mexists{}j:\mBbbZ{}
      (((inl  j  )
      =  case  aa\_max\_ltree(right$_{subtree}$)
          of  inl(intval2)  =>
            inl  imax(val;intval2) 
            |  inr(unitval2)  =>
            inl  val  )
      \mwedge{}  (i  \mleq{}  j))


By

InstConcl  [\mkleeneopen{}case  aa\_max\_ltree(right$_{subtree}$)
                        of  inl(rmaxint)  =>
                          imax(val;rmaxint)
                          |  inr(unitval)  =>
                          val\mkleeneclose{}]  THEN  Auto'\mcdot{}



Home Index