Nuprl Definition : aa_binary_search_tree
aa_binary_search_tree(t) ==
aa_ltree_ind(t;0 
0;v,ltr,rtr,ltrp,rtrp.ltrp
rtrp
case aa_max_ltree(ltr) of inl(maxl) => maxl < v | inr(ul) => 0 0
case aa_min_ltree(rtr) of inl(minr) => v < minr | inr(ur) => 0 0)
Definitions occuring in Statement :
aa_min_ltree: aa_min_ltree(t),
aa_max_ltree: aa_max_ltree(t),
aa_ltree_ind: aa_ltree_ind(x;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val; left_subtree; right_subtree; rec1; rec2]),
le: A B,
and: P Q,
less_than: a < b,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n
FDL editor aliases :
aa_binary_search_tree
aa\_binary\_search\_tree(t) ==
aa\_ltree\_ind(t;0 \mleq{} 0;v,ltr,rtr,ltrp,rtrp.ltrp
\mwedge{} rtrp
\mwedge{} case aa\_max\_ltree(ltr) of inl(maxl) => maxl < v | inr(ul) => 0 \mleq{} 0
\mwedge{} case aa\_min\_ltree(rtr) of inl(minr) => v < minr | inr(ur) => 0 \mleq{} 0)
Date html generated:
2013_03_20-AM-09_52_42
Last ObjectModification:
2012_11_27-AM-10_32_50
Home
Index