Nuprl Definition : min_l_tree
min_l_tree(t;f) ==
  l_tree_ind(t;
             l_tree_leaf(v)
⇒ inr ⋅
             l_tree_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;
                          l\_tree\_leaf(v){}\mRightarrow{}  inr  \mcdot{}  ;
                          l\_tree\_node(v,ltr,rtr){}\mRightarrow{}  ltrm,rtrm.min\_w\_unit\_l\_tree(inl  v;ltrm;f)) 
Date html generated:
2016_05_16-AM-08_44_05
Last ObjectModification:
2016_04_04-PM-00_31_48
Theory : labeled!trees
Home
Index