---

Step * 1 3 of Lemma aa_max_ltree_spec2


1. t : aa_ltree()@i
2. x:aa_ltree(). j:.  ((aa_binary_search_tree(x)  (aa_max_ltree(x) = (inl j )))  aa_bst_member_prop(j;x))
3. j : @i
4. aa_binary_search_tree(t)@i
5. aa_max_ltree(t) = (inl j )@i
 aa_bst_member_prop(j;t)
BY
{ InstHyp [t;j] 2 THEN Auto' }



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


By

InstHyp  [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  2  THEN  Auto'\mcdot{}



Home Index