:: deftheorem defines MakeTree HUFFMAN1:def 8 :
for p, q being finite binary DecoratedTree of IndexedREAL
for k being Nat holds MakeTree (p,q,k) = [k,((Vrootr p) + (Vrootr q))] -tree (p,q);