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] <f[v] then ltrm else rtrm fi 



Definitions occuring in Statement :  l_tree_ind: l_tree_ind bor: p ∨bq ifthenelse: if then else fi  lt_int: i <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