---

Step * of Lemma aa_bst_insert_trial4

t:aa_ltree(). i:.
  (aa_binary_search_tree(t)
   (tp:aa_ltree()
       (aa_binary_search_tree(tp)  (j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;t))))))
BY
{ Auto }

1
1. t : aa_ltree()@i
2. i : @i
3. aa_binary_search_tree(t)@i
 tp:aa_ltree()
   (aa_binary_search_tree(tp)  (j:. (aa_bst_member_prop(j;tp)  (j = i)  aa_bst_member_prop(j;t))))


\mforall{}t:aa\_ltree(\mBbbZ{}).  \mforall{}i:\mBbbZ{}.
    (aa\_binary\_search\_tree(t)
    {}\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;t))))))


By

Auto



Home Index