let SOURCE be non empty finite set ; 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; 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;
( 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 )
;
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;
ex y being Element of BoolBinFinTrees IndexedREAL st S2[n,x,y]
now ( 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 )
;
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;
verum end;
hence
ex
y being
Element of
BoolBinFinTrees IndexedREAL st
S2[
n,
x,
y]
;
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]
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 )
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;
( 1 <= k & k < card SOURCE & 2 <= q . k implies q . (k + 1) = (q . k) - 1 )
assume A14:
( 1
<= k &
k < card SOURCE )
;
( not 2 <= q . k or q . (k + 1) = (q . k) - 1 )
thus
( 2
<= q . k implies
q . (k + 1) = (q . k) - 1 )
verumproof
assume A15:
2
<= q . k
;
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;
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]
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
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;
( 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 )
;
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;
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; verum