Step
*
of Lemma
aa_min_ltree_spec2
t:aa_ltree(). j:.  ((aa_binary_search_tree(t)  (aa_min_ltree(t) = (inl j )))  aa_bst_member_prop(j;t))
BY
{ D 0 THENA ProveWfLemma }
1
1. t : aa_ltree()@i
 j:. ((aa_binary_search_tree(t)  (aa_min_ltree(t) = (inl j )))  aa_bst_member_prop(j;t))
\mforall{}t:aa\_ltree(\mBbbZ{}).  \mforall{}j:\mBbbZ{}.
    ((aa\_binary\_search\_tree(t)  \mwedge{}  (aa\_min\_ltree(t)  =  (inl  j  )))  {}\mRightarrow{}  aa\_bst\_member\_prop(j;t))
By
D  0  THENA  ProveWfLemma
Home
Index