theorem Th27: :: HUFFMAN1:27

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for s, t being finite binary DecoratedTree of IndexedREAL
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds
for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z