Step
*
of Lemma
aa_binary_search_tree_wf
t:aa_ltree(
).
(aa_binary_search_tree(t)
)
BY
{
ProveWfLemma
}
\mforall{}t:aa\_ltree(\mBbbZ{}). (aa\_binary\_search\_tree(t) \mmember{} \mBbbP{})
By
ProveWfLemma
Home
Index
t:aa_ltree(
). (aa_binary_search_tree(t) 
)