:: by Hiroyuki Okazaki , Yuichi Futa and Yasunari Shidama

::

:: Received June 18, 2013

:: Copyright (c) 2013-2021 Association of Mizar Users

definition

let D be non empty set ;

ex b_{1} being DTree-set of D st

for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in b_{1} )

for b_{1}, b_{2} being DTree-set of D st ( for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in b_{1} ) ) & ( for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in b_{2} ) ) holds

b_{1} = b_{2}

end;
func BinFinTrees D -> DTree-set of D means :Def2: :: HUFFMAN1:def 2

for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in it );

existence for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in it );

ex b

for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in b

proof end;

uniqueness for b

( ( dom T is finite & T is binary ) iff T in b

( ( dom T is finite & T is binary ) iff T in b

b

proof end;

:: deftheorem Def2 defines BinFinTrees HUFFMAN1:def 2 :

for D being non empty set

for b_{2} being DTree-set of D holds

( b_{2} = BinFinTrees D iff for T being DecoratedTree of D holds

( ( dom T is finite & T is binary ) iff T in b_{2} ) );

for D being non empty set

for b

( b

( ( dom T is finite & T is binary ) iff T in b

definition

let D be non empty set ;

coherence

{ x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } is non empty Subset of (bool (BinFinTrees D));

end;
func BoolBinFinTrees D -> non empty Subset of (bool (BinFinTrees D)) equals :: HUFFMAN1:def 3

{ x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ;

correctness { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ;

coherence

{ x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } is non empty Subset of (bool (BinFinTrees D));

proof end;

:: deftheorem defines BoolBinFinTrees HUFFMAN1:def 3 :

for D being non empty set holds BoolBinFinTrees D = { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ;

for D being non empty set holds BoolBinFinTrees D = { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ;

definition

let SOURCE be non empty finite set ;

let p be Probability of Trivial-SigmaField SOURCE;

coherence

{ T where T is Element of FinTrees IndexedREAL : ( T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) } is non empty finite Subset of (BinFinTrees IndexedREAL);

end;
let p be Probability of Trivial-SigmaField SOURCE;

func Initial-Trees p -> non empty finite Subset of (BinFinTrees IndexedREAL) equals :: HUFFMAN1:def 4

{ T where T is Element of FinTrees IndexedREAL : ( T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) } ;

correctness { T where T is Element of FinTrees IndexedREAL : ( T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) } ;

coherence

{ T where T is Element of FinTrees IndexedREAL : ( T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) } is non empty finite Subset of (BinFinTrees IndexedREAL);

proof end;

:: deftheorem defines Initial-Trees HUFFMAN1:def 4 :

for SOURCE being non empty finite set

for p being Probability of Trivial-SigmaField SOURCE holds Initial-Trees p = { T where T is Element of FinTrees IndexedREAL : ( T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) } ;

for SOURCE being non empty finite set

for p being Probability of Trivial-SigmaField SOURCE holds Initial-Trees p = { T where T is Element of FinTrees IndexedREAL : ( T is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st T = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) } ;

definition

let p be DecoratedTree of IndexedREAL ;

{} in dom p by TREES_1:22;

then p . {} in rng p by FUNCT_1:3;

then A1: ex x, y being object st

( x in NAT & y in REAL & p . {} = [x,y] ) by ZFMISC_1:def 2;

correctness

coherence

(p . {}) `2 is Real;

by A1;

correctness

coherence

(p . {}) `1 is Nat;

by A1;

end;
{} in dom p by TREES_1:22;

then p . {} in rng p by FUNCT_1:3;

then A1: ex x, y being object st

( x in NAT & y in REAL & p . {} = [x,y] ) by ZFMISC_1:def 2;

correctness

coherence

(p . {}) `2 is Real;

by A1;

correctness

coherence

(p . {}) `1 is Nat;

by A1;

:: deftheorem defines Vrootr HUFFMAN1:def 5 :

for p being DecoratedTree of IndexedREAL holds Vrootr p = (p . {}) `2 ;

for p being DecoratedTree of IndexedREAL holds Vrootr p = (p . {}) `2 ;

:: deftheorem defines Vrootl HUFFMAN1:def 6 :

for p being DecoratedTree of IndexedREAL holds Vrootl p = (p . {}) `1 ;

for p being DecoratedTree of IndexedREAL holds Vrootl p = (p . {}) `1 ;

definition

let T be finite binary DecoratedTree of IndexedREAL ;

let p be Element of dom T;

correctness

coherence

(T . p) `2 is Real;

end;
let p be Element of dom T;

correctness

coherence

(T . p) `2 is Real;

proof end;

:: deftheorem defines Vtree HUFFMAN1:def 7 :

for T being finite binary DecoratedTree of IndexedREAL

for p being Element of dom T holds Vtree p = (T . p) `2 ;

for T being finite binary DecoratedTree of IndexedREAL

for p being Element of dom T holds Vtree p = (T . p) `2 ;

definition

let p, q be finite binary DecoratedTree of IndexedREAL ;

let k be Nat;

coherence

[k,((Vrootr p) + (Vrootr q))] -tree (p,q) is finite binary DecoratedTree of IndexedREAL ;

end;
let k be Nat;

func MakeTree (p,q,k) -> finite binary DecoratedTree of IndexedREAL equals :: HUFFMAN1:def 8

[k,((Vrootr p) + (Vrootr q))] -tree (p,q);

correctness [k,((Vrootr p) + (Vrootr q))] -tree (p,q);

coherence

[k,((Vrootr p) + (Vrootr q))] -tree (p,q) is finite binary DecoratedTree of IndexedREAL ;

proof end;

:: deftheorem defines MakeTree HUFFMAN1:def 8 :

for p, q being finite binary DecoratedTree of IndexedREAL

for k being Nat holds MakeTree (p,q,k) = [k,((Vrootr p) + (Vrootr q))] -tree (p,q);

for p, q being finite binary DecoratedTree of IndexedREAL

for k being Nat holds MakeTree (p,q,k) = [k,((Vrootr p) + (Vrootr q))] -tree (p,q);

definition

let X be non empty finite Subset of (BinFinTrees IndexedREAL);

ex b_{1} being Nat ex L being non empty finite Subset of NAT st

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b_{1} = max L )

for b_{1}, b_{2} being Nat st ex L being non empty finite Subset of NAT st

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b_{1} = max L ) & ex L being non empty finite Subset of NAT st

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b_{2} = max L ) holds

b_{1} = b_{2}
;

end;
func MaxVl X -> Nat means :Def9: :: HUFFMAN1:def 9

ex L being non empty finite Subset of NAT st

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & it = max L );

existence ex L being non empty finite Subset of NAT st

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & it = max L );

ex b

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b

proof end;

uniqueness for b

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b

b

:: deftheorem Def9 defines MaxVl HUFFMAN1:def 9 :

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for b_{2} being Nat holds

( b_{2} = MaxVl X iff ex L being non empty finite Subset of NAT st

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b_{2} = max L ) );

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for b

( b

( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & b

theorem :: HUFFMAN1:1

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for w being finite binary DecoratedTree of IndexedREAL st X = {w} holds

MaxVl X = Vrootl w

for w being finite binary DecoratedTree of IndexedREAL st X = {w} holds

MaxVl X = Vrootl w

proof end;

theorem Th2: :: HUFFMAN1:2

for X, Y, Z being non empty finite Subset of (BinFinTrees IndexedREAL) st Z = X \/ Y holds

MaxVl Z = max ((MaxVl X),(MaxVl Y))

MaxVl Z = max ((MaxVl X),(MaxVl Y))

proof end;

theorem :: HUFFMAN1:3

for X, Z being non empty finite Subset of (BinFinTrees IndexedREAL)

for Y being set st Z = X \ Y holds

MaxVl Z <= MaxVl X

for Y being set st Z = X \ Y holds

MaxVl Z <= MaxVl X

proof end;

theorem :: HUFFMAN1:4

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for p being Element of BinFinTrees IndexedREAL st p in X holds

Vrootl p <= MaxVl X

for p being Element of BinFinTrees IndexedREAL st p in X holds

Vrootl p <= MaxVl X

proof end;

defpred S

Vrootr $2 <= Vrootr q ) );

definition

let X be non empty finite Subset of (BinFinTrees IndexedREAL);

ex b_{1} being finite binary DecoratedTree of IndexedREAL st

( b_{1} in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds

Vrootr b_{1} <= Vrootr q ) )

end;
mode MinValueTree of X -> finite binary DecoratedTree of IndexedREAL means :Def10: :: HUFFMAN1:def 10

( it in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds

Vrootr it <= Vrootr q ) );

existence ( it in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds

Vrootr it <= Vrootr q ) );

ex b

( b

Vrootr b

proof end;

:: deftheorem Def10 defines MinValueTree HUFFMAN1:def 10 :

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for b_{2} being finite binary DecoratedTree of IndexedREAL holds

( b_{2} is MinValueTree of X iff ( b_{2} in X & ( for q being finite binary DecoratedTree of IndexedREAL st q in X holds

Vrootr b_{2} <= Vrootr q ) ) );

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for b

( b

Vrootr b

Lm1: for X being set

for x being object st ex u, v being object st

( u <> v & u in X & v in X ) holds

X \ {x} <> {}

proof end;

Lm2: for X, Y being set

for t, s, z being object st X c= Y & t in Y & s in Y & z in Y holds

(X \ {t,s}) \/ {z} c= Y

proof end;

Lm3: for X being finite set st 2 <= card X holds

ex u, v being object st

( u <> v & u in X & v in X )

proof end;

Lm4: for X being finite set st 1 = card X holds

ex u being object st X = {u}

proof end;

Lm5: for X being finite set

for t, s, z being object st t in X & s in X & t <> s & not z in X holds

card ((X \ {t,s}) \/ {z}) = (card X) - 1

proof end;

theorem Th5: :: HUFFMAN1:5

for SOURCE being non empty finite set

for p being Probability of Trivial-SigmaField SOURCE holds card (Initial-Trees p) = card SOURCE

for p being Probability of Trivial-SigmaField SOURCE holds card (Initial-Trees p) = card SOURCE

proof end;

theorem Th6: :: HUFFMAN1:6

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for s, t being finite binary DecoratedTree of IndexedREAL holds not MakeTree (t,s,((MaxVl X) + 1)) in X

for s, t being finite binary DecoratedTree of IndexedREAL holds not MakeTree (t,s,((MaxVl X) + 1)) in X

proof end;

definition

let X be set ;

coherence

{ (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } is Subset of (bool IndexedREAL);

end;
func LeavesSet X -> Subset of (bool IndexedREAL) equals :: HUFFMAN1:def 11

{ (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ;

correctness { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ;

coherence

{ (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } is Subset of (bool IndexedREAL);

proof end;

:: deftheorem defines LeavesSet HUFFMAN1:def 11 :

for X being set holds LeavesSet X = { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ;

for X being set holds LeavesSet X = { (Leaves p) where p is Element of BinFinTrees IndexedREAL : p in X } ;

theorem Th10: :: HUFFMAN1:10

for s, t being Tree holds Leaves (tree (t,s)) = { (<*0*> ^ p) where p is Element of t : p in Leaves t } \/ { (<*1*> ^ p) where p is Element of s : p in Leaves s }

proof end;

theorem Th11: :: HUFFMAN1:11

for s, t being DecoratedTree

for x being object

for q being FinSequence of NAT st q in dom t holds

(x -tree (t,s)) . (<*0*> ^ q) = t . q

for x being object

for q being FinSequence of NAT st q in dom t holds

(x -tree (t,s)) . (<*0*> ^ q) = t . q

proof end;

theorem Th12: :: HUFFMAN1:12

for s, t being DecoratedTree

for x being object

for q being FinSequence of NAT st q in dom s holds

(x -tree (t,s)) . (<*1*> ^ q) = s . q

for x being object

for q being FinSequence of NAT st q in dom s holds

(x -tree (t,s)) . (<*1*> ^ q) = s . q

proof end;

theorem Th13: :: HUFFMAN1:13

for s, t being DecoratedTree

for x being object holds Leaves (x -tree (t,s)) = (Leaves t) \/ (Leaves s)

for x being object holds Leaves (x -tree (t,s)) = (Leaves t) \/ (Leaves s)

proof end;

theorem Th14: :: HUFFMAN1:14

for k being Nat

for s, t being finite binary DecoratedTree of IndexedREAL holds union (LeavesSet {s,t}) = union (LeavesSet {(MakeTree (t,s,k))})

for s, t being finite binary DecoratedTree of IndexedREAL holds union (LeavesSet {s,t}) = union (LeavesSet {(MakeTree (t,s,k))})

proof end;

theorem Th16: :: HUFFMAN1:16

for x being object

for D being non empty set

for T being finite binary DecoratedTree of D st T = root-tree x holds

Leaves T = {x}

for D being non empty set

for T being finite binary DecoratedTree of D st T = root-tree x holds

Leaves T = {x}

proof end;

definition

let SOURCE be non empty finite set ;

let p be Probability of Trivial-SigmaField SOURCE;

let Tseq be FinSequence of BoolBinFinTrees IndexedREAL;

let q be FinSequence of NAT ;

end;
let p be Probability of Trivial-SigmaField SOURCE;

let Tseq be FinSequence of BoolBinFinTrees IndexedREAL;

let q be FinSequence of NAT ;

pred Tseq,q,p is_constructingBinHuffmanTree means :Def12: :: HUFFMAN1:def 12

( 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 ) );

( 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 ) );

:: 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 ) ) );

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 ) ) );

theorem Th17: :: HUFFMAN1:17

for SOURCE being 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

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

proof end;

definition

let SOURCE be non empty finite set ;

let p be Probability of Trivial-SigmaField SOURCE;

ex b_{1} being finite binary DecoratedTree of IndexedREAL ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st

( Tseq,q,p is_constructingBinHuffmanTree & {b_{1}} = Tseq . (len Tseq) )

end;
let p be Probability of Trivial-SigmaField SOURCE;

mode BinHuffmanTree of p -> finite binary DecoratedTree of IndexedREAL means :Def13: :: HUFFMAN1:def 13

ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st

( Tseq,q,p is_constructingBinHuffmanTree & {it} = Tseq . (len Tseq) );

existence ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st

( Tseq,q,p is_constructingBinHuffmanTree & {it} = Tseq . (len Tseq) );

ex b

( Tseq,q,p is_constructingBinHuffmanTree & {b

proof end;

:: deftheorem Def13 defines BinHuffmanTree HUFFMAN1:def 13 :

for SOURCE being non empty finite set

for p being Probability of Trivial-SigmaField SOURCE

for b_{3} being finite binary DecoratedTree of IndexedREAL holds

( b_{3} is BinHuffmanTree of p iff ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st

( Tseq,q,p is_constructingBinHuffmanTree & {b_{3}} = Tseq . (len Tseq) ) );

for SOURCE being non empty finite set

for p being Probability of Trivial-SigmaField SOURCE

for b

( b

( Tseq,q,p is_constructingBinHuffmanTree & {b

theorem Th18: :: HUFFMAN1:18

for SOURCE being non empty finite set

for p being Probability of Trivial-SigmaField SOURCE holds union (LeavesSet (Initial-Trees p)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }

for p being Probability of Trivial-SigmaField SOURCE holds union (LeavesSet (Initial-Trees p)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }

proof end;

theorem Th19: :: HUFFMAN1:19

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 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})] }

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})] }

proof end;

theorem :: HUFFMAN1:20

for SOURCE being non empty finite set

for p being Probability of Trivial-SigmaField SOURCE

for T being BinHuffmanTree of p holds Leaves T = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }

for p being Probability of Trivial-SigmaField SOURCE

for T being BinHuffmanTree of p holds Leaves T = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }

proof end;

theorem Th21: :: HUFFMAN1:21

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 st Tseq,q,p is_constructingBinHuffmanTree holds

for i being Nat

for T being finite binary DecoratedTree of IndexedREAL

for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds

Vtree t = (Vtree s) + (Vtree r)

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 T being finite binary DecoratedTree of IndexedREAL

for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds

Vtree t = (Vtree s) + (Vtree r)

proof end;

theorem :: HUFFMAN1:22

for SOURCE being non empty finite set

for p being Probability of Trivial-SigmaField SOURCE

for T being BinHuffmanTree of p

for t, s, r being Element of dom T st t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds

Vtree t = (Vtree s) + (Vtree r)

for p being Probability of Trivial-SigmaField SOURCE

for T being BinHuffmanTree of p

for t, s, r being Element of dom T st t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds

Vtree t = (Vtree s) + (Vtree r)

proof end;

theorem Th23: :: HUFFMAN1:23

for X being non empty finite Subset of (BinFinTrees IndexedREAL) st ( 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 ) holds

for s, t, w being finite binary DecoratedTree of IndexedREAL st s in X & t in X & w = MakeTree (t,s,((MaxVl X) + 1)) holds

for p being Element of dom w

for r being Element of NAT st r = (w . p) `1 holds

r <= (MaxVl X) + 1

for p being Element of dom T

for r being Element of NAT st r = (T . p) `1 holds

r <= MaxVl X ) holds

for s, t, w being finite binary DecoratedTree of IndexedREAL st s in X & t in X & w = MakeTree (t,s,((MaxVl X) + 1)) holds

for p being Element of dom w

for r being Element of NAT st r = (w . p) `1 holds

r <= (MaxVl X) + 1

proof end;

theorem Th24: :: HUFFMAN1:24

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 st Tseq,q,p is_constructingBinHuffmanTree holds

for i being Nat st 1 <= i & i < len Tseq holds

for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds

MaxVl Y = (MaxVl X) + 1

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

for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds

MaxVl Y = (MaxVl X) + 1

proof end;

theorem :: HUFFMAN1:25

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 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

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

proof end;

theorem Th26: :: HUFFMAN1:26

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 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

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

proof end;

theorem Th27: :: HUFFMAN1:27

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 st Tseq,q,p is_constructingBinHuffmanTree holds

for i being Nat

for s, t being finite binary DecoratedTree of IndexedREAL

for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds

for z being finite binary DecoratedTree of IndexedREAL st z in X holds

not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z

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 s, t being finite binary DecoratedTree of IndexedREAL

for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds

for z being finite binary DecoratedTree of IndexedREAL st z in X holds

not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z

proof end;

theorem Th28: :: HUFFMAN1:28

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for s, t, w being finite binary DecoratedTree of IndexedREAL st ( 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 ) & ( for p, q being finite binary DecoratedTree of IndexedREAL st p in X & q in X & p <> q holds

(rng p) /\ (rng q) = {} ) & s in X & t in X & s <> t & w in X \ {s,t} holds

(rng (MakeTree (t,s,((MaxVl X) + 1)))) /\ (rng w) = {}

for s, t, w being finite binary DecoratedTree of IndexedREAL st ( 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 ) & ( for p, q being finite binary DecoratedTree of IndexedREAL st p in X & q in X & p <> q holds

(rng p) /\ (rng q) = {} ) & s in X & t in X & s <> t & w in X \ {s,t} holds

(rng (MakeTree (t,s,((MaxVl X) + 1)))) /\ (rng w) = {}

proof end;

theorem Th29: :: HUFFMAN1:29

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 st Tseq,q,p is_constructingBinHuffmanTree holds

for i being Nat

for T, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . i & S in Tseq . i & T <> S holds

(rng T) /\ (rng S) = {}

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 T, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . i & S in Tseq . i & T <> S holds

(rng T) /\ (rng S) = {}

proof end;

theorem Th30: :: HUFFMAN1:30

for X being non empty finite Subset of (BinFinTrees IndexedREAL)

for s, t being finite binary DecoratedTree of IndexedREAL st s is one-to-one & t is one-to-one & t in X & s in X & (rng s) /\ (rng t) = {} & ( for z being finite binary DecoratedTree of IndexedREAL st z in X holds

not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z ) holds

MakeTree (t,s,((MaxVl X) + 1)) is one-to-one

for s, t being finite binary DecoratedTree of IndexedREAL st s is one-to-one & t is one-to-one & t in X & s in X & (rng s) /\ (rng t) = {} & ( for z being finite binary DecoratedTree of IndexedREAL st z in X holds

not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z ) holds

MakeTree (t,s,((MaxVl X) + 1)) is one-to-one

proof end;

theorem Th31: :: HUFFMAN1:31

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 st Tseq,q,p is_constructingBinHuffmanTree holds

for i being Nat

for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds

T is one-to-one

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 T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds

T is one-to-one

proof end;

registration

let SOURCE be non empty finite set ;

let p be Probability of Trivial-SigmaField SOURCE;

coherence

for b_{1} being BinHuffmanTree of p holds b_{1} is one-to-one

end;
let p be Probability of Trivial-SigmaField SOURCE;

coherence

for b

proof end;