Nuprl Definition : bs_tree
bs_tree(E) == {p:bs_treeco(E)| (bs_treeco_size(p))↓}
Definitions occuring in Statement :
bs_treeco_size: bs_treeco_size(p),
bs_treeco: bs_treeco(E),
has-value: (a)↓,
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
bs_treeco: bs_treeco(E),
has-value: (a)↓,
bs_treeco_size: bs_treeco_size(p)
FDL editor aliases :
bs_tree
Latex:
bs\_tree(E) == \{p:bs\_treeco(E)| (bs\_treeco\_size(p))\mdownarrow{}\}
Date html generated:
2016_05_15-PM-01_50_11
Last ObjectModification:
2016_04_07-PM-02_25_20
Theory : tree_1
Home
Index