---

Step * of Lemma aa_min_ltree_spec

t:aa_ltree()
  (aa_binary_search_tree(t)  (i:. (aa_bst_member_prop(i;t)  (j:. (((inl j ) = aa_min_ltree(t))  (i  j ))))))
BY
{ D 0 THENA Auto }

1
1. t : aa_ltree()@i
 aa_binary_search_tree(t)  (i:. (aa_bst_member_prop(i;t)  (j:. (((inl j ) = aa_min_ltree(t))  (i  j )))))


\mforall{}t:aa\_ltree(\mBbbZ{})
    (aa\_binary\_search\_tree(t)
    {}\mRightarrow{}  (\mforall{}i:\mBbbZ{}.  (aa\_bst\_member\_prop(i;t)  {}\mRightarrow{}  (\mexists{}j:\mBbbZ{}.  (((inl  j  )  =  aa\_min\_ltree(t))  \mwedge{}  (i  \mgeq{}  j  ))))))


By

D  0  THENA  Auto



Home Index