Step
*
1
2
1
1
1
of Lemma
aa_max_ltree_spec2
.....truecase..... 
1. t : aa_ltree(
)@i
2. val : 
@i
3. left_subtree : aa_ltree(
)@i
4. right_subtree : aa_ltree(
)@i
5. 
j:
     ((aa_binary_search_tree(left_subtree) 
 (aa_max_ltree(left_subtree) = (inl j )))
     
 aa_bst_member_prop(j;left_subtree))@i
6. 
j:
     ((aa_binary_search_tree(right_subtree) 
 (aa_max_ltree(right_subtree) = (inl j )))
     
 aa_bst_member_prop(j;right_subtree))@i
7. j : 
@i
8. aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))@i
9. x : 
10. aa_max_ltree(right_subtree) = (inl x )
11. (inl imax(val;x) ) = (inl j )@i
12. x = j
13. val 
 x
 aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree))
BY
{ ((RepUR ``aa_binary_search_tree`` 8 THEN Fold `aa_binary_search_tree` 8 THEN D 8 THEN InstHyp [
j
] 6 THEN Auto'
    THEN RepUR ``aa_bst_member_prop`` 0
    )
   THEN Fold `aa_bst_member_prop` 0 THEN Auto'
   ) }
1
1. t : aa_ltree(
)@i
2. val : 
@i
3. left_subtree : aa_ltree(
)@i
4. right_subtree : aa_ltree(
)@i
5. 
j:
     ((aa_binary_search_tree(left_subtree) 
 (aa_max_ltree(left_subtree) = (inl j )))
     
 aa_bst_member_prop(j;left_subtree))@i
6. 
j:
     ((aa_binary_search_tree(right_subtree) 
 (aa_max_ltree(right_subtree) = (inl j )))
     
 aa_bst_member_prop(j;right_subtree))@i
7. j : 
@i
8. aa_binary_search_tree(left_subtree)@i
9. aa_binary_search_tree(right_subtree)@i
10. case aa_max_ltree(left_subtree) of inl(maxl) => maxl < val | inr(ul) => 0 
 0@i
11. case aa_min_ltree(right_subtree) of inl(minr) => val < minr | inr(ur) => 0 
 0@i
12. x : 
13. aa_max_ltree(right_subtree) = (inl x )
14. (inl imax(val;x) ) = (inl j )@i
15. x = j
16. val 
 x
17. aa_bst_member_prop(j;right_subtree)
 (val = j) 
 ((j < val) 
 aa_bst_member_prop(j;left_subtree)) 
 ((val < j) 
 aa_bst_member_prop(j;right_subtree))
.....truecase..... 
1.  t  :  aa\_ltree(\mBbbZ{})@i
2.  val  :  \mBbbZ{}@i
3.  left$_{subtree}$  :  aa\_ltree(\mBbbZ{})@i
4.  right$_{subtree}$  :  aa\_ltree(\mBbbZ{})@i
5.  \mforall{}j:\mBbbZ{}
          ((aa\_binary\_search\_tree(left$_{subtree}$)  \mwedge{}  (aa\_max\_ltree(left$_\mbackslash{}ff\000C7bsubtree}$)  =  (inl  j  )))
          {}\mRightarrow{}  aa\_bst\_member\_prop(j;left$_{subtree}$))@i
6.  \mforall{}j:\mBbbZ{}
          ((aa\_binary\_search\_tree(right$_{subtree}$)  \mwedge{}  (aa\_max\_ltree(right$_\mbackslash{}\000Cff7bsubtree}$)  =  (inl  j  )))
          {}\mRightarrow{}  aa\_bst\_member\_prop(j;right$_{subtree}$))@i
7.  j  :  \mBbbZ{}@i
8.  aa\_binary\_search\_tree(aa\_lt\_node(val;left$_{subtree}$;right$_{sub\000Ctree}$))@i
9.  x  :  \mBbbZ{}
10.  aa\_max\_ltree(right$_{subtree}$)  =  (inl  x  )
11.  (inl  imax(val;x)  )  =  (inl  j  )@i
12.  x  =  j
13.  val  \mleq{}  x
\mvdash{}  aa\_bst\_member\_prop(j;aa\_lt\_node(val;left$_{subtree}$;right$_{subtr\000Cee}$))
By
((RepUR  ``aa\_binary\_search\_tree``  8  THEN  Fold  `aa\_binary\_search\_tree`  8  THEN  D  8  THEN  InstHyp  [\mkleeneopen{}j\mkleeneclose{}
    ]  6  THEN  Auto'\mcdot{}
    THEN  RepUR  ``aa\_bst\_member\_prop``  0
    )
  THEN  Fold  `aa\_bst\_member\_prop`  0  THEN  Auto'
  )
Home
Index