let SOURCE be 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
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
let p be 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
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
let Tseq be 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
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
let q be FinSequence of NAT ; ( Tseq,q,p is_constructingBinHuffmanTree implies for i being Nat st 1 <= i & i <= len Tseq holds
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } )
assume A1:
Tseq,q,p is_constructingBinHuffmanTree
; for i being Nat st 1 <= i & i <= len Tseq holds
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
defpred S2[ Nat] means ( $1 < len Tseq implies union (LeavesSet (Tseq . ($1 + 1))) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } );
A2:
S2[ 0 ]
by Th18, A1;
A3:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A4:
S2[
k]
;
S2[k + 1]
assume A5:
k + 1
< len Tseq
;
union (LeavesSet (Tseq . ((k + 1) + 1))) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
A6:
k <= k + 1
by NAT_1:11;
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 A7:
(
Tseq . (k + 1) = X &
Y = X \ {s} &
w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} &
Tseq . ((k + 1) + 1) = (X \ {t,s}) \/ {w} )
by A1, A5, NAT_1:11;
A8:
(
w = MakeTree (
t,
s,
((MaxVl X) + 1)) or
w = MakeTree (
s,
t,
((MaxVl X) + 1)) )
by A7, TARSKI:def 2;
A9:
LeavesSet (Tseq . ((k + 1) + 1)) = (LeavesSet (X \ {t,s})) \/ (LeavesSet {w})
by Th8, A7;
A10:
union (LeavesSet {w}) = union (LeavesSet {t,s})
by Th14, A8;
A11:
union (LeavesSet (Tseq . ((k + 1) + 1))) =
(union (LeavesSet (X \ {t,s}))) \/ (union (LeavesSet {w}))
by ZFMISC_1:78, A9
.=
union ((LeavesSet (X \ {t,s})) \/ (LeavesSet {t,s}))
by ZFMISC_1:78, A10
.=
union (LeavesSet ((X \ {t,s}) \/ {t,s}))
by Th8
;
A12:
(
s in X &
t in Y )
by Def10;
then
(
t in X & not
t in {s} )
by A7, XBOOLE_0:def 5;
hence
union (LeavesSet (Tseq . ((k + 1) + 1))) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
by A12, A6, A4, A5, XXREAL_0:2, A7, A11, XBOOLE_1:45, ZFMISC_1:32;
verum
end;
A13:
for k being Nat holds S2[k]
from NAT_1:sch 2(A2, A3);
let i be Nat; ( 1 <= i & i <= len Tseq implies union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } )
assume A14:
( 1 <= i & i <= len Tseq )
; union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
then reconsider i1 = i - 1 as Nat by NAT_1:21;
i - 1 < (len Tseq) - 0
by XREAL_1:15, A14;
then
union (LeavesSet (Tseq . (i1 + 1))) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
by A13;
hence
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
; verum