theorem Th24: :: HUFFMAN1:24

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 st 1 <= i & i < len Tseq holds
for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds
MaxVl Y = (MaxVl X) + 1