---

Step * 1 of Lemma aa_max_ltree_spec2


1. t : aa_ltree()@i
 j:. ((aa_binary_search_tree(t)  (aa_max_ltree(t) = (inl j )))  aa_bst_member_prop(j;t))
BY
{ InstLemma `aa_ltree-induction` [; t.j:
                                              ((aa_binary_search_tree(t)  (aa_max_ltree(t) = (inl j )))
                                               aa_bst_member_prop(j;t))] THEN Auto' }

1
1. t : aa_ltree()@i
2. j : @i
3. aa_binary_search_tree(aa_lt_leaf())@i
4. aa_max_ltree(aa_lt_leaf()) = (inl j )@i
 aa_bst_member_prop(j;aa_lt_leaf())

2
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. aa_max_ltree(aa_lt_node(val;left_subtree;right_subtree)) = (inl j )@i
 aa_bst_member_prop(j;aa_lt_node(val;left_subtree;right_subtree))

3
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)



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


By

InstLemma  `aa\_ltree-induction`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};  \mkleeneopen{}\mlambda{}\msubtwo{}t.\mforall{}j:\mBbbZ{}
                                                                                        ((aa\_binary\_search\_tree(t)
                                                                                        \mwedge{}  (aa\_max\_ltree(t)  =  (inl  j  )))
                                                                                        {}\mRightarrow{}  aa\_bst\_member\_prop(j;t))\mkleeneclose{}]  THEN  Auto'\mcdot{}\mcdot{}



Home Index