:: deftheorem Def12 defines is_constructingBinHuffmanTree HUFFMAN1:def 12 :
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 holds
( Tseq,q,p is_constructingBinHuffmanTree iff ( Tseq . 1 = Initial-Trees p & len Tseq = card SOURCE & ( for i being Nat st 1 <= i & i < len Tseq holds
ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex v being finite binary DecoratedTree of IndexedREAL st
( Tseq . i = X & Y = X \ {s} & v in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (i + 1) = (X \ {t,s}) \/ {v} ) ) & ex T being finite binary DecoratedTree of IndexedREAL st {T} = Tseq . (len Tseq) & dom q = Seg (card SOURCE) & ( for k being Nat st k in Seg (card SOURCE) holds
( q . k = card (Tseq . k) & q . k <> 0 ) ) & ( for k being Nat st k < card SOURCE holds
q . (k + 1) = (q . 1) - k ) & ( for k being Nat st 1 <= k & k < card SOURCE holds
2 <= q . k ) ) );