Nuprl Definition : aa_bst_member
aa_bst_member(i;t) ==  aa_ltree_ind(t;ff;v,ltr,rtr,ltrm,rtrm.(v =
 i) 
if i <z v then ltrm else rtrm fi )
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]), 
eq_int: (i =
 j), 
bor: p 
q, 
lt_int: i <z j, 
ifthenelse: if b then t else f fi , 
bfalse: ff
FDL editor aliases : 
aa_bst_member
aa\_bst\_member(i;t)  ==
    aa\_ltree\_ind(t;ff;v,ltr,rtr,ltrm,rtrm.(v  =\msubz{}  i)  \mvee{}\msubb{}if  i  <z  v  then  ltrm  else  rtrm  fi  )
Date html generated:
2013_03_20-AM-09_52_32
Last ObjectModification:
2012_11_27-AM-10_32_47
Home
Index