---

Step * 1 1 of Lemma aa_bst_insert_sublemma_left


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
12. aa_bst_member_prop(j;tp)  ((j = i)  aa_bst_member_prop(j;left_subtree))
13. aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;left_subtree)
14. (j = i)
 aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree))
BY
{ ((((Unfold `aa_bst_member_prop` 11 THEN Reduce 11) THEN D 11) THEN Auto') THEN Try ((D 11 THEN 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. val = j
12. aa_bst_member_prop(j;tp)  ((j = i)  aa_bst_member_prop(j;left_subtree))
13. aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;left_subtree)
14. (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 < val@i
12. aa_ltree_ind(tp;False;val,left_subtree,right_subtree,rec1,rec2.(val = j)
 ((j < val)  rec1)
 ((val < j)  rec2))@i
13. aa_bst_member_prop(j;tp)  ((j = i)  aa_bst_member_prop(j;left_subtree))
14. aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;left_subtree)
15. (j = i)
 aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree))

3
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. val < j@i
12. aa_ltree_ind(right_subtree;False;val,left_subtree,right_subtree,rec1,rec2.(val = j)
 ((j < val)  rec1)
 ((val < j)  rec2))@i
13. aa_bst_member_prop(j;tp)  ((j = i)  aa_bst_member_prop(j;left_subtree))
14. aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;left_subtree)
15. (j = i)
 aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree))



1.  left$_{subtree}$  :  aa\_ltree(\mBbbZ{})@i
2.  right$_{subtree}$  :  aa\_ltree(\mBbbZ{})@i
3.  tp  :  aa\_ltree(\mBbbZ{})@i
4.  val  :  \mBbbZ{}@i
5.  i  :  \mBbbZ{}@i
6.  aa\_binary\_search\_tree(tp)@i
7.  aa\_binary\_search\_tree(aa\_lt\_node(val;left$_{subtree}$;right$_{sub\000Ctree}$))@i
8.  i  <  val@i
9.  \mforall{}j:\mBbbZ{}.  (aa\_bst\_member\_prop(j;tp)  \mLeftarrow{}{}\mRightarrow{}  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;left$_{subtree\mbackslash{}ff7\000Cd$))@i
10.  j  :  \mBbbZ{}@i
11.  aa\_bst\_member\_prop(j;aa\_lt\_node(val;tp;right$_{subtree}$))@i
12.  aa\_bst\_member\_prop(j;tp)  {}\mRightarrow{}  ((j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;left$_{subtree}$\000C))
13.  aa\_bst\_member\_prop(j;tp)  \mLeftarrow{}{}  (j  =  i)  \mvee{}  aa\_bst\_member\_prop(j;left$_{subtree}$)
14.  \mneg{}(j  =  i)
\mvdash{}  aa\_bst\_member\_prop(j;aa\_lt\_node(val;left$_{subtree}$;right$_{subtr\000Cee}$))


By

((((Unfold  `aa\_bst\_member\_prop`  11  THEN  Reduce  11\mcdot{})  THEN  D  11)  THEN  Auto')\mcdot{}
  THEN  Try  ((D  11  THEN  Auto'))
  )



Home Index