:: deftheorem defines Vtree HUFFMAN1:def 7 :
for T being finite binary DecoratedTree of IndexedREAL
for p being Element of dom T holds Vtree p = (T . p) `2 ;