Nuprl Definition : member_bs_tree
member_bs_tree(E;x;tr) == case(tr)null=>Falseleaf(v)=>v = x ∈ Enode(a,v,b)=>mema,memb.(v = x ∈ E) ∨ mema ∨ memb
Definitions occuring in Statement :
bs_tree_ind: bs_tree_ind,
or: P ∨ Q,
false: False,
equal: s = t ∈ T
Definitions occuring in definition :
bs_tree_ind: bs_tree_ind,
false: False,
equal: s = t ∈ T,
or: P ∨ Q
FDL editor aliases :
member_bs_tree
Latex:
member\_bs\_tree(E;x;tr) ==
case(tr)
null=>False
leaf(v)=>v = x
node(a,v,b)=>mema,memb.(v = x) \mvee{} mema \mvee{} memb
Date html generated:
2016_05_15-PM-01_51_04
Last ObjectModification:
2016_04_07-PM-06_59_06
Theory : tree_1
Home
Index