Nuprl Definition : bs_l_tree_member
bs_l_tree_member(x;t;f) ==
l_tree_ind(t;
Leaf(v)⇒ tt;
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
Latex:
bs\_l\_tree\_member(x;t;f) ==
l\_tree\_ind(t;
Leaf(v){}\mRightarrow{} tt;
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:
2018_05_22-PM-09_40_00
Last ObjectModification:
2012_06_25-PM-07_39_37
Theory : labeled!trees
Home
Index