Nuprl Definition : bs_l_tree_member
bs_l_tree_member(x;t;f) ==
l_tree_ind(t;
l_tree_leaf(v)⇒ tt;
l_tree_node(v,ltr,rtr)⇒ ltrm,rtrm.(f[x] =z f[v]) ∨bif f[x] <z f[v] then ltrm else rtrm fi )
Definitions occuring in Statement :
l_tree_ind: l_tree_ind,
bor: p ∨bq,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
eq_int: (i =z j),
btrue: tt,
so_apply: x[s]
FDL editor aliases :
bs_l_tree_member
bs\_l\_tree\_member(x;t;f) ==
l\_tree\_ind(t;
l\_tree\_leaf(v){}\mRightarrow{} tt;
l\_tree\_node(v,ltr,rtr){}\mRightarrow{} ltrm,rtrm.(f[x] =\msubz{} f[v])
\mvee{}\msubb{}if f[x] <z f[v] then ltrm else rtrm fi )
Date html generated:
2015_07_17-AM-07_41_53
Last ObjectModification:
2012_06_25-PM-07_39_37
Home
Index