:: deftheorem Def13 defines BinHuffmanTree HUFFMAN1:def 13 :
for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for b₃ being finite binary DecoratedTree of IndexedREAL holds
( b₃ is BinHuffmanTree of p iff ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st
( Tseq,q,p is_constructingBinHuffmanTree & {b₃} = Tseq . (len Tseq) ) );