---

Step * 1 1 of Lemma aa_max_ltree_spec2


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

1
1. t : aa_ltree()@i
2. j : @i
3. aa_binary_search_tree(aa_lt_leaf())@i
4. (inr  ) = (inl j )@i
 aa_bst_member_prop(j;aa_lt_leaf())



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


By

RepUR  ``aa\_max\_ltree``  (-1)  THEN  Auto'



Home Index