---

Step * 1 2 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(aa_lt_node(val;left_subtree;right_subtree))@i
9. case aa_max_ltree(right_subtree) of inl(intval2) => inl imax(val;intval2)  | inr(unitval2) => inl val  = (inl j )@i
 aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree))
BY
{ (GenHypAtAddr (-1) [2;1] THEN DVar `v' THEN Reduce (-1) THEN MaAutoSimpHyp Auto (-1)) }

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(aa_lt_node(val;left_subtree;right_subtree))@i
9. x : 
10. aa_max_ltree(right_subtree) = (inl x )
11. (inl imax(val;x) ) = (inl j )@i
12. imax(val;x) = j
 aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree))

2
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(aa_lt_node(val;left_subtree;right_subtree))@i
9. y : Unit
10. aa_max_ltree(right_subtree) = (inr y )
11. (inl val ) = (inl j )@i
12. val = j
 aa_bst_member_prop(j;aa_lt_node(val;left_subtree;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(aa\_lt\_node(val;left$_{subtree}$;right$_{sub\000Ctree}$))@i
9.  case  aa\_max\_ltree(right$_{subtree}$)
of  inl(intval2)  =>
  inl  imax(val;intval2) 
  |  inr(unitval2)  =>
  inl  val 
=  (inl  j  )@i
\mvdash{}  aa\_bst\_member\_prop(j;aa\_lt\_node(val;left$_{subtree}$;right$_{subtr\000Cee}$))


By

(GenHypAtAddr  (-1)  [2;1]  THEN  DVar  `v'  THEN  Reduce  (-1)  THEN  MaAutoSimpHyp  Auto  (-1))



Home Index