---

Step * 1 2 1 2 of Lemma aa_bst_insert_trial4


1. t : aa_ltree()@i
2. i : @i
3. aa_binary_search_tree(t)@i
4. val : @i
5. left_subtree : aa_ltree()@i
6. right_subtree : aa_ltree()@i
7. aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))@i
8. aa_binary_search_tree(left_subtree)
9. aa_binary_search_tree(right_subtree)
10. case aa_max_ltree(left_subtree) of inl(maxl) => maxl < val | inr(ul) => 0  0
11. case aa_min_ltree(right_subtree) of inl(minr) => val < minr | inr(ur) => 0  0
12. tpl : aa_ltree()@i
13. aa_binary_search_tree(tpl)@i
14. j:. (aa_bst_member_prop(j;tpl)  (j = i)  aa_bst_member_prop(j;left_subtree))@i
15. tpr : aa_ltree()@i
16. aa_binary_search_tree(tpr)@i
17. j:. (aa_bst_member_prop(j;tpr)  (j = i)  aa_bst_member_prop(j;right_subtree))@i
18. i = val
19. j : @i
20. (j = i)  aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree))@i
 aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree))
BY
{ (D (-1) THEN Auto'  THEN (Assert j = val THEN (Auto'  THEN (RepUR ``aa_bst_member_prop`` 0 THEN Auto' )))) }



1.  t  :  aa\_ltree(\mBbbZ{})@i
2.  i  :  \mBbbZ{}@i
3.  aa\_binary\_search\_tree(t)@i
4.  val  :  \mBbbZ{}@i
5.  left$_{subtree}$  :  aa\_ltree(\mBbbZ{})@i
6.  right$_{subtree}$  :  aa\_ltree(\mBbbZ{})@i
7.  aa\_binary\_search\_tree(aa\_lt\_node(val;left$_{subtree}$;right$_{sub\000Ctree}$))@i
8.  aa\_binary\_search\_tree(left$_{subtree}$)
9.  aa\_binary\_search\_tree(right$_{subtree}$)
10.  case  aa\_max\_ltree(left$_{subtree}$)  of  inl(maxl)  =>  maxl  <  val  |  inr(ul)  =>  \000C0  \mleq{}  0
11.  case  aa\_min\_ltree(right$_{subtree}$)  of  inl(minr)  =>  val  <  minr  |  inr(ur)  =>\000C  0  \mleq{}  0
12.  tpl  :  aa\_ltree(\mBbbZ{})@i
13.  aa\_binary\_search\_tree(tpl)@i
14.  \mforall{}j:\mBbbZ{}.  (aa\_bst\_member\_prop(j;tpl)  \mLeftarrow{}{}\mRightarrow{}  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;left$_{subtree\mbackslash{}f\000Cf7d$))@i
15.  tpr  :  aa\_ltree(\mBbbZ{})@i
16.  aa\_binary\_search\_tree(tpr)@i
17.  \mforall{}j:\mBbbZ{}.  (aa\_bst\_member\_prop(j;tpr)  \mLeftarrow{}{}\mRightarrow{}  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;right$_{subtree\mbackslash{}\000Cff7d$))@i
18.  i  =  val
19.  j  :  \mBbbZ{}@i
20.  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;aa\_lt\_node(val;left$_{subtree}$;right$\mbackslash{}ff\000C5f{subtree}$))@i
\mvdash{}  aa\_bst\_member\_prop(j;aa\_lt\_node(val;left$_{subtree}$;right$_{subtr\000Cee}$))


By

(D  (-1)
  THEN  Auto'
  \mcdot{}
  THEN  (Assert  \mkleeneopen{}j  =  val\mkleeneclose{}\mcdot{}  THEN  (Auto'  \mcdot{}  THEN  (RepUR  ``aa\_bst\_member\_prop``  0  THEN  Auto'  \mcdot{}))))



Home Index