---

Step * of Lemma aa_max_ltree_spec2

t:aa_ltree(). j:.  ((aa_binary_search_tree(t)  (aa_max_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_max_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\_max\_ltree(t)  =  (inl  j  )))  {}\mRightarrow{}  aa\_bst\_member\_prop(j;t))


By

D  0  THENA  ProveWfLemma



Home Index