---

Step * 1 2 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)
 tp:aa_ltree()
   (aa_binary_search_tree(tp)
    (j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree)))))
BY
{ BoolCase i <z val THEN Auto' }

1
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. i < val
 tp:aa_ltree()
   (aa_binary_search_tree(tp)
    (j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree)))))

2
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. val  i
 tp:aa_ltree()
   (aa_binary_search_tree(tp)
    (j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree)))))



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.  \mneg{}(i  =  val)
\mvdash{}  \mexists{}tp:aa\_ltree(\mBbbZ{})
      (aa\_binary\_search\_tree(tp)
      \mwedge{}  (\mforall{}j:\mBbbZ{}
                (aa\_bst\_member\_prop(j;tp)
                \mLeftarrow{}{}\mRightarrow{}  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;aa\_lt\_node(val;left$_{subtree}$;right\000C$_{subtree}$)))))


By

BoolCase  \mkleeneopen{}i  <z  val\mkleeneclose{}  THEN  Auto'\mcdot{}



Home Index