---

Step * of Lemma aa_max_ltree_spec

t:aa_ltree()
  (aa_binary_search_tree(t)  (i:. (aa_bst_member_prop(i;t)  (j:. (((inl j ) = aa_max_ltree(t))  (i  j))))))
BY
{ D 0 THENA Auto }

1
1. t : aa_ltree()@i
 aa_binary_search_tree(t)  (i:. (aa_bst_member_prop(i;t)  (j:. (((inl j ) = aa_max_ltree(t))  (i  j)))))


\mforall{}t:aa\_ltree(\mBbbZ{})
    (aa\_binary\_search\_tree(t)
    {}\mRightarrow{}  (\mforall{}i:\mBbbZ{}.  (aa\_bst\_member\_prop(i;t)  {}\mRightarrow{}  (\mexists{}j:\mBbbZ{}.  (((inl  j  )  =  aa\_max\_ltree(t))  \mwedge{}  (i  \mleq{}  j))))))


By

D  0  THENA  Auto



Home Index