:: deftheorem defines Vrootr HUFFMAN1:def 5 :
for p being DecoratedTree of IndexedREAL holds Vrootr p = (p . {}) `2 ;