---

Step * of Lemma aa_bst_member_property2

ltr,rtr:aa_ltree(). val,i:.
  ((aa_binary_search_tree(aa_lt_node(val;ltr;rtr))  aa_bst_member_prop(i;ltr))  (i < val))
BY
{ ((Auto THEN RepUR ``aa_binary_search_tree`` (-2) THEN Fold `aa_binary_search_tree` (-2) THEN D (-2) THEN D (-2))
   THEN D (-2)
   ) }

1
1. ltr : aa_ltree()@i
2. rtr : aa_ltree()@i
3. val : @i
4. i : @i
5. aa_binary_search_tree(ltr)@i
6. aa_binary_search_tree(rtr)@i
7. case aa_max_ltree(ltr) of inl(maxl) => maxl < val | inr(ul) => 0  0@i
8. case aa_min_ltree(rtr) of inl(minr) => val < minr | inr(ur) => 0  0@i
9. aa_bst_member_prop(i;ltr)@i
 i < val


\mforall{}ltr,rtr:aa\_ltree(\mBbbZ{}).  \mforall{}val,i:\mBbbZ{}.
    ((aa\_binary\_search\_tree(aa\_lt\_node(val;ltr;rtr))  \mwedge{}  aa\_bst\_member\_prop(i;ltr))  {}\mRightarrow{}  (i  <  val))


By

((Auto  THEN  RepUR  ``aa\_binary\_search\_tree``  (-2)  THEN  Fold  `aa\_binary\_search\_tree`  (-2)  THEN  D  (-2)
    THEN  D  (-2)
    )
  THEN  D  (-2)
  )



Home Index