---

Step * 1 1 of Lemma aa_bst_member_property2


1. ltr : aa_ltree()@i
2. rtr : aa_ltree()@i
3. val : @i
4. i : @i
5. aa_binary_search_tree(ltr)@i
6. aa_binary_search_tree(rtr)@i
7. x : 
8. aa_max_ltree(ltr) = (inl x )
9. x < val@i
10. case aa_min_ltree(rtr) of inl(minr) => val < minr | inr(ur) => 0  0@i
11. aa_bst_member_prop(i;ltr)@i
 i < val
BY
{ InstLemma `aa_max_ltree_spec` [ltr;i] THEN Auto' THEN D (-1) THEN Assert x = j THEN MaAuto }



1.  ltr  :  aa\_ltree(\mBbbZ{})@i
2.  rtr  :  aa\_ltree(\mBbbZ{})@i
3.  val  :  \mBbbZ{}@i
4.  i  :  \mBbbZ{}@i
5.  aa\_binary\_search\_tree(ltr)@i
6.  aa\_binary\_search\_tree(rtr)@i
7.  x  :  \mBbbZ{}
8.  aa\_max\_ltree(ltr)  =  (inl  x  )
9.  x  <  val@i
10.  case  aa\_min\_ltree(rtr)  of  inl(minr)  =>  val  <  minr  |  inr(ur)  =>  0  \mleq{}  0@i
11.  aa\_bst\_member\_prop(i;ltr)@i
\mvdash{}  i  <  val


By

InstLemma  `aa\_max\_ltree\_spec`  [\mkleeneopen{}ltr\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  THEN  Auto'  THEN  D  (-1)  THEN  Assert  \mkleeneopen{}x  =  j\mkleeneclose{}  THEN  MaAuto\mcdot{}



Home Index