Nuprl Definition : tree-height
tree-height(t) == tree_ind(t; tree_leaf(x)⇒ 0; tree_node(l,r)⇒ lh,rh.imax(lh;rh) + 1)
Definitions occuring in Statement :
tree_ind: tree_ind,
imax: imax(a;b),
add: n + m,
natural_number: $n
Definitions occuring in definition :
tree_ind: tree_ind,
add: n + m,
imax: imax(a;b),
natural_number: $n
FDL editor aliases :
tree-height
Latex:
tree-height(t) == tree\_ind(t; tree\_leaf(x){}\mRightarrow{} 0; tree\_node(l,r){}\mRightarrow{} lh,rh.imax(lh;rh) + 1)
Date html generated:
2017_10_01-AM-08_30_41
Last ObjectModification:
2017_05_02-AM-11_51_34
Theory : tree_1
Home
Index