Nuprl Definition : tree
tree(E) == {p:treeco(E)| (treeco_size(p))↓}
Definitions occuring in Statement :
treeco_size: treeco_size(p),
treeco: treeco(E),
has-value: (a)↓,
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
treeco: treeco(E),
has-value: (a)↓,
treeco_size: treeco_size(p)
FDL editor aliases :
tree
Latex:
tree(E) == \{p:treeco(E)| (treeco\_size(p))\mdownarrow{}\}
Date html generated:
2016_05_15-PM-01_49_25
Last ObjectModification:
2015_09_23-AM-07_37_18
Theory : tree_1
Home
Index