---

Step * 1 of Lemma aa_min_ltree_spec


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

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

2
1. t : aa_ltree()@i
2. val : @i
3. left_subtree : aa_ltree()@i
4. right_subtree : aa_ltree()@i
5. aa_binary_search_tree(left_subtree)
 (i:. (aa_bst_member_prop(i;left_subtree)  (j:. (((inl j ) = aa_min_ltree(left_subtree))  (i  j )))))@i
6. aa_binary_search_tree(right_subtree)
 (i:. (aa_bst_member_prop(i;right_subtree)  (j:. (((inl j ) = aa_min_ltree(right_subtree))  (i  j )))))@i
7. aa_binary_search_tree(aa_lt_node(val;left_subtree;right_subtree))@i
8. i : @i
9. aa_bst_member_prop(i;aa_lt_node(val;left_subtree;right_subtree))@i
 j:. (((inl j ) = aa_min_ltree(aa_lt_node(val;left_subtree;right_subtree)))  (i  j ))

3
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_min_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_min_ltree(t))  (i  j ))



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


By

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



Home Index