---

Step * of Lemma aa_bst_insert_sublemma_left

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;left_subtree))))
   (j:
        (aa_bst_member_prop(j;aa_lt_node(val;tp;right_subtree))
         (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;left_subtree))@i
10. j : @i
11. aa_bst_member_prop(j;aa_lt_node(val;tp;right_subtree))@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;left_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;tp;right_subtree))


\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;left$_{subtree\mbackslash{}f\000Cf7d$))))
    {}\mRightarrow{}  (\mforall{}j:\mBbbZ{}
                (aa\_bst\_member\_prop(j;aa\_lt\_node(val;tp;right$_{subtree}$))
                \mLeftarrow{}{}\mRightarrow{}  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;aa\_lt\_node(val;left$_{subtree}$;right\000C$_{subtree}$)))))


By

Auto



Home Index