Nuprl Definition : min_l_tree
min_l_tree(t;f) == l_tree_ind(t; Leaf(v)⇒ inr ⋅ ; Node(v,ltr,rtr)⇒ ltrm,rtrm.min_w_unit_l_tree(inl v;ltrm;f))
Definitions occuring in Statement :
min_w_unit_l_tree: min_w_unit_l_tree(u1;u2;f),
l_tree_ind: l_tree_ind,
it: ⋅,
inr: inr x ,
inl: inl x
Definitions occuring in definition :
l_tree_ind: l_tree_ind,
inr: inr x ,
it: ⋅,
min_w_unit_l_tree: min_w_unit_l_tree(u1;u2;f),
inl: inl x
FDL editor aliases :
min_l_tree
Latex:
min\_l\_tree(t;f) ==
l\_tree\_ind(t;
Leaf(v){}\mRightarrow{} inr \mcdot{} ;
Node(v,ltr,rtr){}\mRightarrow{} ltrm,rtrm.min\_w\_unit\_l\_tree(inl v;ltrm;f))
Date html generated:
2018_05_22-PM-09_39_53
Last ObjectModification:
2016_04_04-PM-00_31_48
Theory : labeled!trees
Home
Index