---

Step * 1 1 of Lemma aa_bst_insert_trial4


1. t : aa_ltree()@i
2. i : @i
3. aa_binary_search_tree(t)@i
4. aa_binary_search_tree(aa_lt_leaf())@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_leaf()))))
BY
{ (InstConcl [aa_lt_node(i;aa_lt_leaf();aa_lt_leaf())] THEN RepUR ``aa_bst_member_prop`` 0
   THEN Auto
   THEN Try (Complete ((SplitOrHyps THEN Auto)))
   THEN RepUR ``aa_binary_search_tree aa_max_ltree aa_min_ltree`` 0
   THEN Auto) }



1.  t  :  aa\_ltree(\mBbbZ{})@i
2.  i  :  \mBbbZ{}@i
3.  aa\_binary\_search\_tree(t)@i
4.  aa\_binary\_search\_tree(aa\_lt\_leaf())@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\_leaf()))))


By

(InstConcl  [\mkleeneopen{}aa\_lt\_node(i;aa\_lt\_leaf();aa\_lt\_leaf())\mkleeneclose{}]  THEN  RepUR  ``aa\_bst\_member\_prop``  0\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((SplitOrHyps  THEN  Auto)))
  THEN  RepUR  ``aa\_binary\_search\_tree  aa\_max\_ltree  aa\_min\_ltree``  0
  THEN  Auto)



Home Index