---

Step * 1 1 of Lemma aa_max_ltree_spec


1. t : aa_ltree()@i
2. aa_binary_search_tree(aa_lt_leaf())@i
3. i : @i
4. aa_bst_member_prop(i;aa_lt_leaf())@i
 j:. (((inl j ) = aa_max_ltree(aa_lt_leaf()))  (i  j))
BY
{ RepUR ``aa_bst_member_prop`` 4 THEN Auto }



1.  t  :  aa\_ltree(\mBbbZ{})@i
2.  aa\_binary\_search\_tree(aa\_lt\_leaf())@i
3.  i  :  \mBbbZ{}@i
4.  aa\_bst\_member\_prop(i;aa\_lt\_leaf())@i
\mvdash{}  \mexists{}j:\mBbbZ{}.  (((inl  j  )  =  aa\_max\_ltree(aa\_lt\_leaf()))  \mwedge{}  (i  \mleq{}  j))


By

RepUR  ``aa\_bst\_member\_prop``  4  THEN  Auto



Home Index