---

Step * of Lemma aa_max_ltree_spec3

t:aa_ltree(). (((aa_binary_search_tree(t)  (i:. aa_bst_member_prop(i;t)))  (aa_max_ltree(t) = (inr  )))  False)
BY
{ (Auto THEN D 3) }

1
1. t : aa_ltree()@i
2. aa_binary_search_tree(t)@i
3. i : @i
4. aa_bst_member_prop(i;t)@i
5. aa_max_ltree(t) = (inr  )@i
 False


\mforall{}t:aa\_ltree(\mBbbZ{})
    (((aa\_binary\_search\_tree(t)  \mwedge{}  (\mexists{}i:\mBbbZ{}.  aa\_bst\_member\_prop(i;t)))  \mwedge{}  (aa\_max\_ltree(t)  =  (inr  \mcdot{}  )))
    {}\mRightarrow{}  False)


By

(Auto  THEN  D  3)



Home Index