---

Step * 1 3 of Lemma aa_max_ltree_spec


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



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


By

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



Home Index