---

Step * of Lemma aa_bst_insert_sublemma_right

left_subtree,right_subtree,tp:aa_ltree(). val,i:.
  ((aa_binary_search_tree(tp)
   aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))
   (i > val)
   (j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;right_subtree))))
   (j:
        (aa_bst_member_prop(j;aa_lt_node(val;left_subtree;tp))
         (j = i)  aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree)))))
BY
{ Auto }

1
1. left_subtree : aa_ltree()@i
2. right_subtree : aa_ltree()@i
3. tp : aa_ltree()@i
4. val : @i
5. i : @i
6. aa_binary_search_tree(tp)@i
7. aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))@i
8. i > val@i
9. j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;right_subtree))@i
10. j : @i
11. aa_bst_member_prop(j;aa_lt_node(val;left_subtree;tp))@i
 (j = i)  aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree))

2
1. left_subtree : aa_ltree()@i
2. right_subtree : aa_ltree()@i
3. tp : aa_ltree()@i
4. val : @i
5. i : @i
6. aa_binary_search_tree(tp)@i
7. aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))@i
8. i > val@i
9. j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;right_subtree))@i
10. j : @i
11. (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;tp))


\mforall{}left$_{subtree}$,right$_{subtree}$,tp:aa\_ltree(\mBbbZ{}).  \mforall{}val,i:\mBbbZ{}\000C.
    ((aa\_binary\_search\_tree(tp)
    \mwedge{}  aa\_binary\_search\_tree(aa\_lt\_node(val;left$_{subtree}$;right$_{su\000Cbtree}$))
    \mwedge{}  (i  >  val)
    \mwedge{}  (\mforall{}j:\mBbbZ{}.  (aa\_bst\_member\_prop(j;tp)  \mLeftarrow{}{}\mRightarrow{}  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;right$_{subtree\mbackslash{}\000Cff7d$))))
    {}\mRightarrow{}  (\mforall{}j:\mBbbZ{}
                (aa\_bst\_member\_prop(j;aa\_lt\_node(val;left$_{subtree}$;tp))
                \mLeftarrow{}{}\mRightarrow{}  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;aa\_lt\_node(val;left$_{subtree}$;right\000C$_{subtree}$)))))


By

Auto



Home Index