---

Step * 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(left_subtree)
 (tp:aa_ltree()
     (aa_binary_search_tree(tp)
      (j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;left_subtree)))))@i
8. aa_binary_search_tree(right_subtree)
 (tp:aa_ltree()
     (aa_binary_search_tree(tp)
      (j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;right_subtree)))))@i
9. aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))@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)))))
BY
{ (Duplicate
   (-1)
THEN ((( RepUR ``aa_binary_search_tree`` (-1) THEN Fold `aa_binary_search_tree` (-1) THEN ID (-1) THEN ID (-1) 
        THEN (D 7 THEN Auto' )
        THEN (D 7 THEN Auto'))
       THEN ExRepD
       )
      THEN (RenameVar `tpl' 12 THEN (RenameVar `tpr' 15 THEN BoolCase (i = 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
 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)
 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(left$_{subtree}$)
{}\mRightarrow{}  (\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;left$_{subtre\000Ce}$)))))@i
8.  aa\_binary\_search\_tree(right$_{subtree}$)
{}\mRightarrow{}  (\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;right$_{subtr\000Cee}$)))))@i
9.  aa\_binary\_search\_tree(aa\_lt\_node(val;left$_{subtree}$;right$_{sub\000Ctree}$))@i
\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

(Duplicate
  (-1)\mcdot{}
THEN  (((...
                THEN  (D  7  THEN  Auto'  \mcdot{})
                THEN  (D  7  THEN  Auto'))
              THEN  ExRepD
              )
            THEN  (RenameVar  `tpl'  12\mcdot{}  THEN  (RenameVar  `tpr'  15\mcdot{}  THEN  BoolCase  \mkleeneopen{}(i  =\msubz{}  val)\mkleeneclose{}\mcdot{}  THEN  Auto'))
            )
)



Home Index