Nuprl Definition : aa_bst_member_prop
aa_bst_member_prop(i;t) == aa_ltree_ind(t;False;v,ltr,rtr,ltrm,rtrm.(v = i) 
((i < v) 
ltrm) ((v < i) rtrm))
Definitions occuring in Statement :
aa_ltree_ind: aa_ltree_ind(x;leaf;val,left_subtree,right_subtree,rec1,rec2.node[val; left_subtree; right_subtree; rec1; rec2]),
or: P Q,
and: P Q,
false: False,
less_than: a < b,
int: 
,
equal: s = t
FDL editor aliases :
aa_bst_member_prop
aa\_bst\_member\_prop(i;t) ==
aa\_ltree\_ind(t;False;v,ltr,rtr,ltrm,rtrm.(v = i) \mvee{} ((i < v) \mwedge{} ltrm) \mvee{} ((v < i) \mwedge{} rtrm))
Date html generated:
2013_03_20-AM-09_52_35
Last ObjectModification:
2012_11_27-AM-10_32_48
Home
Index