let SOURCE be non empty finite set ; :: thesis: for p being Probability of Trivial-SigmaField SOURCE ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree
let p be Probability of Trivial-SigmaField SOURCE; :: thesis: ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree
defpred S2[ Nat, set , set ] means ( ex u, v being object st
( u <> v & u in $2 & v in $2 ) implies ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex w being finite binary DecoratedTree of IndexedREAL st
( $2 = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & $3 = (X \ {t,s}) \/ {w} ) );
A1: for n being Nat st 1 <= n & n < card SOURCE holds
for x being Element of BoolBinFinTrees IndexedREAL ex y being Element of BoolBinFinTrees IndexedREAL st S2[n,x,y]
proof
let n be Nat; :: thesis: ( 1 <= n & n < card SOURCE implies for x being Element of BoolBinFinTrees IndexedREAL ex y being Element of BoolBinFinTrees IndexedREAL st S2[n,x,y] )
assume ( 1 <= n & n < card SOURCE ) ; :: thesis: for x being Element of BoolBinFinTrees IndexedREAL ex y being Element of BoolBinFinTrees IndexedREAL st S2[n,x,y]
let x be Element of BoolBinFinTrees IndexedREAL; :: thesis: ex y being Element of BoolBinFinTrees IndexedREAL st S2[n,x,y]
now :: thesis: ( ex u, v being object st
( u <> v & u in x & v in x ) implies ex y being Element of BoolBinFinTrees IndexedREAL ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex w being finite binary DecoratedTree of IndexedREAL st
( x = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & y = (X \ {t,s}) \/ {w} ) )
assume ex u, v being object st
( u <> v & u in x & v in x ) ; :: thesis: ex y being Element of BoolBinFinTrees IndexedREAL ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex w being finite binary DecoratedTree of IndexedREAL st
( x = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & y = (X \ {t,s}) \/ {w} )
then consider u, v being object such that
A2: ( u <> v & u in x & v in x ) ;
x in BoolBinFinTrees IndexedREAL ;
then ex z being Element of bool (BinFinTrees IndexedREAL) st
( z = x & z is finite & z <> {} ) ;
then reconsider X = x as non empty finite Subset of (BinFinTrees IndexedREAL) ;
set s = the MinValueTree of X;
set Y = X \ { the MinValueTree of X};
reconsider Y = X \ { the MinValueTree of X} as Subset of (BinFinTrees IndexedREAL) ;
reconsider Y = Y as non empty finite Subset of (BinFinTrees IndexedREAL) by A2, Lm1;
set t = the MinValueTree of Y;
set w = MakeTree ( the MinValueTree of Y, the MinValueTree of X,((MaxVl X) + 1));
A3: MakeTree ( the MinValueTree of Y, the MinValueTree of X,((MaxVl X) + 1)) in {(MakeTree ( the MinValueTree of Y, the MinValueTree of X,((MaxVl X) + 1))),(MakeTree ( the MinValueTree of X, the MinValueTree of Y,((MaxVl X) + 1)))} by TARSKI:def 2;
set y = (X \ { the MinValueTree of Y, the MinValueTree of X}) \/ {(MakeTree ( the MinValueTree of Y, the MinValueTree of X,((MaxVl X) + 1)))};
A4: ( the MinValueTree of X in X & the MinValueTree of Y in Y ) by Def10;
( dom (MakeTree ( the MinValueTree of Y, the MinValueTree of X,((MaxVl X) + 1))) is finite & dom (MakeTree ( the MinValueTree of Y, the MinValueTree of X,((MaxVl X) + 1))) is binary & dom (MakeTree ( the MinValueTree of X, the MinValueTree of Y,((MaxVl X) + 1))) is finite & dom (MakeTree ( the MinValueTree of X, the MinValueTree of Y,((MaxVl X) + 1))) is binary ) by BINTREE1:def 3;
then MakeTree ( the MinValueTree of Y, the MinValueTree of X,((MaxVl X) + 1)) in BinFinTrees IndexedREAL by Def2;
then (X \ { the MinValueTree of Y, the MinValueTree of X}) \/ {(MakeTree ( the MinValueTree of Y, the MinValueTree of X,((MaxVl X) + 1)))} c= BinFinTrees IndexedREAL by A4, Lm2;
then (X \ { the MinValueTree of Y, the MinValueTree of X}) \/ {(MakeTree ( the MinValueTree of Y, the MinValueTree of X,((MaxVl X) + 1)))} in BoolBinFinTrees IndexedREAL ;
hence ex y being Element of BoolBinFinTrees IndexedREAL ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex w being finite binary DecoratedTree of IndexedREAL st
( x = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & y = (X \ {t,s}) \/ {w} ) by A3; :: thesis: verum
end;
hence ex y being Element of BoolBinFinTrees IndexedREAL st S2[n,x,y] ; :: thesis: verum
end;
Initial-Trees p in BoolBinFinTrees IndexedREAL ;
then reconsider ITS = Initial-Trees p as Element of BoolBinFinTrees IndexedREAL ;
consider Tseq being FinSequence of BoolBinFinTrees IndexedREAL such that
A5: ( len Tseq = card SOURCE & ( Tseq . 1 = ITS or card SOURCE = 0 ) & ( for n being Nat st 1 <= n & n < card SOURCE holds
S2[n,Tseq . n,Tseq . (n + 1)] ) ) from RECDEF_1:sch 4(A1);
 defpred S3[ object , object ] means ex X being finite set st
( Tseq . $1 = X & $2 = card X & $2 <> 0 );
A6: for k being Nat st k in Seg (card SOURCE) holds
ex x being Element of NAT st S3[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (card SOURCE) implies ex x being Element of NAT st S3[k,x] )
assume k in Seg (card SOURCE) ; :: thesis: ex x being Element of NAT st S3[k,x]
then k in dom Tseq by A5, FINSEQ_1:def 3;
then Tseq . k in rng Tseq by FUNCT_1:3;
then Tseq . k in BoolBinFinTrees IndexedREAL by FINSEQ_1:def 4, TARSKI:def 3;
then A7: ex x being Element of bool (BinFinTrees IndexedREAL) st
( x = Tseq . k & x is finite & x <> {} ) ;
then reconsider X = Tseq . k as finite set ;
take x = card X; :: thesis: S3[k,x]
thus S3[k,x] by A7; :: thesis: verum
end;
consider q being FinSequence of NAT such that
A8: ( dom q = Seg (card SOURCE) & ( for k being Nat st k in Seg (card SOURCE) holds
S3[k,q . k] ) ) from FINSEQ_1:sch 5(A6);
 A9: for k being Nat st k in Seg (card SOURCE) holds
( q . k = card (Tseq . k) & q . k <> 0 )
proof
let k be Nat; :: thesis: ( k in Seg (card SOURCE) implies ( q . k = card (Tseq . k) & q . k <> 0 ) )
assume k in Seg (card SOURCE) ; :: thesis: ( q . k = card (Tseq . k) & q . k <> 0 )
then ex X being finite set st
( Tseq . k = X & q . k = card X & q . k <> 0 ) by A8;
hence ( q . k = card (Tseq . k) & q . k <> 0 ) ; :: thesis: verum
end;
A10: card (Initial-Trees p) = card SOURCE by Th5;
1 <= card SOURCE by NAT_1:14;
then A11: 1 in Seg (card SOURCE) by FINSEQ_1:1;
then A12: q . 1 = card SOURCE by A5, A9, A10;
A13: for k being Nat st 1 <= k & k < card SOURCE & 2 <= q . k holds
q . (k + 1) = (q . k) - 1
proof
let k be Nat; :: thesis: ( 1 <= k & k < card SOURCE & 2 <= q . k implies q . (k + 1) = (q . k) - 1 )
assume A14: ( 1 <= k & k < card SOURCE ) ; :: thesis: ( not 2 <= q . k or q . (k + 1) = (q . k) - 1 )
thus ( 2 <= q . k implies q . (k + 1) = (q . k) - 1 ) :: thesis: verum
proof
assume A15: 2 <= q . k ; :: thesis: q . (k + 1) = (q . k) - 1
A16: ( ex u, v being object st
( u <> v & u in Tseq . k & v in Tseq . k ) implies ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex w being finite binary DecoratedTree of IndexedREAL st
( Tseq . k = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (k + 1) = (X \ {t,s}) \/ {w} ) ) by A5, A14;
k in Seg (card SOURCE) by FINSEQ_1:1, A14;
then A17: q . k = card (Tseq . k) by A9;
A18: 1 <= k + 1 by NAT_1:11;
k + 1 <= card SOURCE by NAT_1:13, A14;
then k + 1 in Seg (card SOURCE) by A18, FINSEQ_1:1;
then A19: q . (k + 1) = card (Tseq . (k + 1)) by A9;
consider Tseqk being finite set such that
A20: ( Tseq . k = Tseqk & q . k = card Tseqk & q . k <> 0 ) by FINSEQ_1:1, A14, A8;
consider X, Y being non empty finite Subset of (BinFinTrees IndexedREAL), s being MinValueTree of X, t being MinValueTree of Y, w being finite binary DecoratedTree of IndexedREAL such that
A21: ( Tseq . k = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (k + 1) = (X \ {t,s}) \/ {w} ) by Lm3, A20, A15, A16;
A22: ( s in X & t in Y ) by Def10;
then ( t in X & not t in {s} ) by A21, XBOOLE_0:def 5;
then A23: ( t in X & t <> s ) by TARSKI:def 1;
( not MakeTree (t,s,((MaxVl X) + 1)) in X & not MakeTree (s,t,((MaxVl X) + 1)) in X ) by Th6;
then not w in X by A21, TARSKI:def 2;
hence q . (k + 1) = (q . k) - 1 by A22, A17, A19, A21, Lm5, A23; :: thesis: verum
end;
end;
defpred S4[ Nat] means ( $1 < card SOURCE implies q . ($1 + 1) = (q . 1) - $1 );
A24: S4[ 0 ] ;
A25: for n being Nat st S4[n] holds
S4[n + 1]
proof
let n be Nat; :: thesis: ( S4[n] implies S4[n + 1] )
assume A26: S4[n] ; :: thesis: S4[n + 1]
assume A27: n + 1 < card SOURCE ; :: thesis: q . ((n + 1) + 1) = (q . 1) - (n + 1)
A28: n <= n + 1 by NAT_1:11;
( 1 <= n + 1 & n + 1 <= card SOURCE ) by A27, NAT_1:11;
then n + 1 in Seg (card SOURCE) by FINSEQ_1:1;
then A29: 1 <= q . (n + 1) by NAT_1:14, A9;
A30: 1 + 1 <= q . (n + 1)
proof
assume not 1 + 1 <= q . (n + 1) ; :: thesis: contradiction
then q . (n + 1) <= 1 by NAT_1:13;
then 1 = (q . 1) - n by A28, A26, A27, XXREAL_0:2, XXREAL_0:1, A29;
hence contradiction by A27, A11, A5, A9, A10; :: thesis: verum
end;
q . ((n + 1) + 1) = (q . (n + 1)) - 1 by A13, A30, A27, NAT_1:11;
hence q . ((n + 1) + 1) = (q . 1) - (n + 1) by A28, A26, A27, XXREAL_0:2; :: thesis: verum
end;
A31: for n being Nat holds S4[n] from NAT_1:sch 2(A24, A25);
 A32: for n being Nat st 1 <= n & n < card SOURCE holds
2 <= q . n
proof
let n be Nat; :: thesis: ( 1 <= n & n < card SOURCE implies 2 <= q . n )
assume A33: ( 1 <= n & n < card SOURCE ) ; :: thesis: 2 <= q . n
then reconsider n0 = n - 1 as Nat by NAT_1:21;
n - 1 < n - 0 by XREAL_1:15;
then n0 < card SOURCE by A33, XXREAL_0:2;
then A34: q . (n0 + 1) = (q . 1) - n0 by A31;
n + 1 <= card SOURCE by NAT_1:13, A33;
then (n + 1) - 1 <= (card SOURCE) - 1 by XREAL_1:9;
then ((q . 1) + 1) - ((card SOURCE) - 1) <= ((q . 1) + 1) - n by XREAL_1:13;
hence 2 <= q . n by A12, A34; :: thesis: verum
end;
A35: for k being Nat st 1 <= k & k < 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 w being finite binary DecoratedTree of IndexedREAL st
( Tseq . k = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (k + 1) = (X \ {t,s}) \/ {w} )
proof
let k be Nat; :: thesis: ( 1 <= k & k < len Tseq implies ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex w being finite binary DecoratedTree of IndexedREAL st
( Tseq . k = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (k + 1) = (X \ {t,s}) \/ {w} ) )
assume A36: ( 1 <= k & k < len Tseq ) ; :: thesis: ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex w being finite binary DecoratedTree of IndexedREAL st
( Tseq . k = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (k + 1) = (X \ {t,s}) \/ {w} )
A37: ( ex u, v being object st
( u <> v & u in Tseq . k & v in Tseq . k ) implies ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex w being finite binary DecoratedTree of IndexedREAL st
( Tseq . k = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (k + 1) = (X \ {t,s}) \/ {w} ) ) by A5, A36;
ex Tseqk being finite set st
( Tseq . k = Tseqk & q . k = card Tseqk & q . k <> 0 ) by FINSEQ_1:1, A36, A5, A8;
hence ex X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) ex s being MinValueTree of X ex t being MinValueTree of Y ex w being finite binary DecoratedTree of IndexedREAL st
( Tseq . k = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (k + 1) = (X \ {t,s}) \/ {w} ) by A37, Lm3, A36, A32, A5; :: thesis: verum
end;
reconsider n1 = (card SOURCE) - 1 as Nat by NAT_1:14, NAT_1:21;
(card SOURCE) - 1 < (card SOURCE) - 0 by XREAL_1:15;
then A38: q . (n1 + 1) = (q . 1) - n1 by A31;
A39: card SOURCE in Seg (card SOURCE) by FINSEQ_1:3;
consider Tseqk being finite set such that
A40: ( Tseq . (card SOURCE) = Tseqk & q . (card SOURCE) = card Tseqk & q . (card SOURCE) <> 0 ) by FINSEQ_1:3, A8;
consider u being object such that
A41: Tseqk = {u} by Lm4, A12, A38, A40;
card SOURCE in dom Tseq by FINSEQ_1:def 3, A5, A39;
then A42: Tseq . (card SOURCE) in rng Tseq by FUNCT_1:3;
A43: u in Tseqk by TARSKI:def 1, A41;
then reconsider T = u as DecoratedTree of IndexedREAL by A40, A42;
A44: ( dom T is finite & T is binary ) by A43, Def2, A40, A42;
reconsider T = T as finite binary DecoratedTree of IndexedREAL by A44, FINSET_1:10;
{T} = Tseq . (len Tseq) by A40, A41, A5;
hence ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree by A35, A5, A8, A9, A31, A32, Def12; :: thesis: verum