---

Step * 1 2 of Lemma aa_bst_member_property2r


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. case aa_max_ltree(ltr) of inl(maxl) => maxl < val | inr(ul) => 0  0@i
8. y : Unit
9. aa_min_ltree(rtr) = (inr y )
10. case inr y  of inl(minr) => val < minr | inr(ur) => 0  0@i
11. aa_bst_member_prop(i;rtr)@i
 i > val
BY
{ InstLemma `aa_min_ltree_spec3` [rtr] THEN Auto' }

1
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. case aa_max_ltree(ltr) of inl(maxl) => maxl < val | inr(ul) => 0  0@i
8. y : Unit
9. aa_min_ltree(rtr) = (inr y )
10. case inr y  of inl(minr) => val < minr | inr(ur) => 0  0@i
11. aa_bst_member_prop(i;rtr)@i
 i:. aa_bst_member_prop(i;rtr)

2
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. case aa_max_ltree(ltr) of inl(maxl) => maxl < val | inr(ul) => 0  0@i
8. y : Unit
9. aa_min_ltree(rtr) = (inr y )
10. case inr y  of inl(minr) => val < minr | inr(ur) => 0  0@i
11. aa_bst_member_prop(i;rtr)@i
 aa_min_ltree(rtr) = (inr  )



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.  case  aa\_max\_ltree(ltr)  of  inl(maxl)  =>  maxl  <  val  |  inr(ul)  =>  0  \mleq{}  0@i
8.  y  :  Unit
9.  aa\_min\_ltree(rtr)  =  (inr  y  )
10.  case  inr  y    of  inl(minr)  =>  val  <  minr  |  inr(ur)  =>  0  \mleq{}  0@i
11.  aa\_bst\_member\_prop(i;rtr)@i
\mvdash{}  i  >  val


By

InstLemma  `aa\_min\_ltree\_spec3`  [\mkleeneopen{}rtr\mkleeneclose{}]  THEN  Auto'\mcdot{}



Home Index