---

Step * 1 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. (inr  ) = (inl j )@i
 aa_bst_member_prop(j;aa_lt_leaf())
BY
{ MaAutoSimpHyp Auto 4 }



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


By

MaAutoSimpHyp  Auto  4\mcdot{}



Home Index