Nuprl Definition : max_l_tree
max_l_tree(t;f) ==
l_tree_ind(t;
l_tree_leaf(v)⇒ inr ⋅ ;
l_tree_node(v,ltr,rtr)⇒ ltrm,rtrm.max_w_unit_l_tree(inl v;rtrm;f))
Definitions occuring in Statement :
max_w_unit_l_tree: max_w_unit_l_tree(u1;u2;f),
l_tree_ind: l_tree_ind,
it: ⋅,
inr: inr x ,
inl: inl x
FDL editor aliases :
max_l_tree
max\_l\_tree(t;f) ==
l\_tree\_ind(t;
l\_tree\_leaf(v){}\mRightarrow{} inr \mcdot{} ;
l\_tree\_node(v,ltr,rtr){}\mRightarrow{} ltrm,rtrm.max\_w\_unit\_l\_tree(inl v;rtrm;f))
Date html generated:
2015_07_17-AM-07_41_46
Last ObjectModification:
2012_06_25-PM-06_33_05
Home
Index