let SOURCE be non empty finite set ; :: thesis: 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
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i holds
for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X
let p be Probability of Trivial-SigmaField SOURCE; :: thesis: for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i holds
for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X
let Tseq be FinSequence of BoolBinFinTrees IndexedREAL; :: thesis: for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i holds
for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X
let q be FinSequence of NAT ; :: thesis: ( Tseq,q,p is_constructingBinHuffmanTree implies for i being Nat
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i holds
for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X )
assume A1: Tseq,q,p is_constructingBinHuffmanTree ; :: thesis: for i being Nat
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i holds
for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X
defpred S<sub>2</sub>[ Nat] means ( 1 <= $1 & $1 <= len Tseq implies for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . $1 holds
for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X );
A2: S₂[ 0 ] ;
A3: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A4: S₂[i] ; :: thesis: S₂[i + 1]
assume A5: ( 1 <= i + 1 & i + 1 <= len Tseq ) ; :: thesis: for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . (i + 1) holds
for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X
let W be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: ( W = Tseq . (i + 1) implies for T being finite binary DecoratedTree of IndexedREAL st T in W holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl W )
assume A6: W = Tseq . (i + 1) ; :: thesis: for T being finite binary DecoratedTree of IndexedREAL st T in W holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl W
let d be finite binary DecoratedTree of IndexedREAL ; :: thesis: ( d in W implies for p being Element of dom d
for r being Element of NAT st r = (d . p) `1 holds
r <= MaxVl W )
assume A7: d in W ; :: thesis: for p being Element of dom d
for r being Element of NAT st r = (d . p) `1 holds
r <= MaxVl W

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: for p being Element of dom d
for r being Element of NAT st r = (d . p) `1 holds
r <= MaxVl W

then consider d0 being Element of FinTrees IndexedREAL such that
A8: ( d0 = d & d0 is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st d0 = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) by A1, A6, A7;
thus for p being Element of dom d
for r being Element of NAT st r = (d . p) `1 holds
r <= MaxVl W :: thesis: verum

proof

let p be Element of dom d; :: thesis: for r being Element of NAT st r = (d . p) `1 holds
r <= MaxVl W
let r be Element of NAT ; :: thesis: ( r = (d . p) `1 implies r <= MaxVl W )
assume A9: r = (d . p) `1 ; :: thesis: r <= MaxVl W
dom d = {{}} by TREES_1:29, A8;
then A10: r = Vrootl d by A9, TARSKI:def 1;
consider L being non empty finite Subset of NAT such that
A11: ( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in W } & MaxVl W = max L ) by Def9;
( dom d is finite & dom d is binary ) by BINTREE1:def 3;
then reconsider px = d as Element of BinFinTrees IndexedREAL by Def2;
Vrootl px in L by A7, A11;
hence r <= MaxVl W by A10, A11, XXREAL_2:def 8; :: thesis: verum

end;

end;

suppose A12: i <> 0 ; :: thesis: for p being Element of dom d
for r being Element of NAT st r = (d . p) `1 holds
r <= MaxVl W

then A13: ( 1 <= i & i < len Tseq ) by A5, XXREAL_0:2, NAT_1:16, NAT_1:14;
then 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
A14: ( Tseq . i = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (i + 1) = (X \ {t,s}) \/ {w} ) by A1;
A15: for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X by A4, A12, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A14;
A16: ( w = MakeTree (t,s,((MaxVl X) + 1)) or w = MakeTree (s,t,((MaxVl X) + 1)) ) by A14, TARSKI:def 2;
A17: ( s in X & t in Y ) by Def10;
A18: ( t in X & not t in {s} ) by A17, A14, XBOOLE_0:def 5;
A19: MaxVl W = (MaxVl X) + 1 by A13, A14, Th24, A1, A6;
thus for p being Element of dom d
for r being Element of NAT st r = (d . p) `1 holds
r <= MaxVl W :: thesis: verum

proof

let p be Element of dom d; :: thesis: for r being Element of NAT st r = (d . p) `1 holds
r <= MaxVl W
let r be Element of NAT ; :: thesis: ( r = (d . p) `1 implies r <= MaxVl W )
assume A20: r = (d . p) `1 ; :: thesis: r <= MaxVl W

per cases ( d in X \ {t,s} or d in {w} ) by XBOOLE_0:def 3, A14, A6, A7;

suppose d in X \ {t,s} ; :: thesis: r <= MaxVl W

then d in X by XBOOLE_0:def 5;
then r <= MaxVl X by A20, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A12, A14, A4;
hence r <= MaxVl W by A19, XXREAL_0:2, NAT_1:16; :: thesis: verum

end;

suppose d in {w} ; :: thesis: r <= MaxVl W

then d = w by TARSKI:def 1;
hence r <= MaxVl W by A17, A19, A16, A20, A18, Th23, A15; :: thesis: verum

end;

end;

end;

end;

end;

end;

A21: for i being Nat holds S₂[i] from NAT_1:sch 2(A2, A3);
let i be Nat; :: thesis: for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i holds
for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X
let X be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: ( X = Tseq . i implies for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X )
assume A22: X = Tseq . i ; :: thesis: for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X
let T be finite binary DecoratedTree of IndexedREAL ; :: thesis: ( T in X implies for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X )
assume A23: T in X ; :: thesis: for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X
i in dom Tseq by A22, FUNCT_1:def 2;
then ( 1 <= i & i <= len Tseq ) by FINSEQ_3:25;
hence for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X by A22, A23, A21; :: thesis: verum