:: Constructing Binary {H}uffman Tree
:: by Hiroyuki Okazaki , Yuichi Futa and Yasunari Shidama
::
:: Received June 18, 2013
:: Copyright (c) 2013 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FINSEQ_1, FUNCT_1, XXREAL_0, ORDINAL4,
RELAT_1, TREES_1, XBOOLE_0, FINSET_1, TARSKI, TREES_2, FUNCT_2, CARD_1,
ZFMISC_1, MCART_1, NAT_1, ARYTM_3, TREES_A, ARYTM_1, TREES_3, REAL_1,
BINTREE1, ORDINAL1, TREES_4, HUFFMAN1, PROB_1, RANDOM_1, UPROOTS;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_2, DOMAIN_1, FUNCOP_1, FINSET_1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, XXREAL_2, FINSEQ_1,
TREES_1, RVSUM_1, TREES_2, TREES_3, TREES_4, PROB_1, BINTREE1, RANDOM_1;
constructors DOMAIN_1, XXREAL_2, RELSET_1, WELLORD2, BINTREE1, RVSUM_1,
RANDOM_1, ARYTM_1, TREES_4, RFINSEQ2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, TREES_3,
FINSET_1, XREAL_0, NAT_1, FINSEQ_1, TREES_1, TREES_2, CARD_1, RELSET_1,
MEMBERED, BINTREE1, XTUPLE_0, VALUED_0, RVSUM_1, NUMBERS, FRAENKEL,
XXREAL_2, FUNCOP_1, TREES_4;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities TREES_2, TREES_3, TREES_4;
expansions BINTREE1;
theorems TARSKI, ZFMISC_1, FINSEQ_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
FINSEQ_2, TREES_1, TREES_2, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1,
XXREAL_0, TREES_4, ORDINAL1, CARD_1, FINSET_1, TREES_3, XREAL_0,
BINTREE1, CARD_2, XXREAL_2, WELLORD2, FINSEQ_3;
schemes NAT_1, XBOOLE_0, FINSEQ_1, RECDEF_1, FUNCT_2, FRAENKEL;
begin :: Constructing Binary Decoded Trees
registration
let D be non empty set, x be Element of D;
cluster root-tree x -> binary for DecoratedTree;
coherence by FUNCT_2:def 1;
end;
definition
func IndexedREAL -> set equals
[:NAT,REAL:];
correctness;
end;
registration
cluster IndexedREAL -> non empty;
coherence;
end;
definition
let D be non empty set;
func BinFinTrees D -> DTree-set of D means :Def2:
for T being DecoratedTree of D holds
dom T is finite & T is binary iff T in it;
existence
proof
defpred S1[element] means ex T being DecoratedTree of D st
$1 = T & dom T is finite & T is binary;
consider X being set such that
A1: for x being element holds
x in X iff x in Trees D & S1[x] from XBOOLE_0:sch 1;
set T = the finite binary DecoratedTree of D;
dom the finite binary DecoratedTree of D is binary by BINTREE1:def 3;
then A2: not X is empty by A1,TREES_3: def 7;
now
let x be element;
assume x in X;
then x in Trees D by A1;
hence x is DecoratedTree of D;
end;
then reconsider X as DTree-set of D by A2, TREES_3: def 6;
take X;
let T be DecoratedTree of D;
thus dom T is finite & T is binary implies T in X by A1,TREES_3:def 7;
assume T in X;
then ex t being DecoratedTree of D st
T = t & (dom t is finite & t is binary) by A1;
hence dom T is finite & T is binary;
end;
uniqueness
proof
let T1, T2 be DTree-set of D;
assume that
A3: for T being DecoratedTree of D holds
(dom T is finite & T is binary) iff T in T1 and
A4: for T being DecoratedTree of D holds
(dom T is finite & T is binary) iff T in T2;
thus T1 c= T2
proof
let x be element;
assume A5: x in T1;
then reconsider T = x as DecoratedTree of D;
dom T is finite & T is binary by A3, A5;
hence x in T2 by A4;
end;
let x be element;
assume A6: x in T2;
then reconsider T = x as DecoratedTree of D;
dom T is finite & T is binary by A4, A6;
hence x in T1 by A3;
end;
end;
definition
let D be non empty set;
func BoolBinFinTrees D -> non empty Subset of bool BinFinTrees D equals
{x where x is Element of bool BinFinTrees D: x is finite & x <> {} };
correctness
proof
set L = {x where x is Element of bool BinFinTrees D
: x is finite & x <> {} };
A1:now let z be element;
assume z in L; then
ex x be Element of bool BinFinTrees D st x=z & x is finite & x <> {};
hence z in bool BinFinTrees D;
end;
consider z be element such that
A2: z in D by XBOOLE_0:def 1;
reconsider z as Element of D by A2;
set T = the finite binary DecoratedTree of D;
dom T is finite & dom T is binary by BINTREE1:def 3; then
T in BinFinTrees D by Def2; then
reconsider x= {T} as Element of bool BinFinTrees D by ZFMISC_1:31;
x in L;
hence thesis by A1,TARSKI:def 3;
end;
end;
reserve SOURCE for non empty finite set,
p for Probability of Trivial-SigmaField SOURCE,
Tseq for FinSequence of BoolBinFinTrees IndexedREAL,
q for FinSequence of NAT;
definition
let SOURCE,p;
func Initial-Trees(p)
-> non empty finite Subset of BinFinTrees IndexedREAL equals
{T where T is Element of FinTrees IndexedREAL :
T is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st
T = root-tree [ (canFS SOURCE)".x, p.{x} ] };
correctness
proof
reconsider fcs = (canFS SOURCE)" as Function of SOURCE, Seg (card SOURCE)
by FINSEQ_1:95;
set S = {T where T is Element of FinTrees IndexedREAL :
T is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st
T = root-tree [ (canFS SOURCE)".x, p.{x} ] };
now let z be element;
assume z in S;
then ex T be Element of FinTrees IndexedREAL st
z= T & T is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st
T = root-tree [ (canFS SOURCE)".x, p.{x} ];
then reconsider z0 = z as finite binary DecoratedTree of IndexedREAL;
dom z0 is finite & dom z0 is binary by BINTREE1:def 3;
hence z in BinFinTrees IndexedREAL by Def2;
end;
then reconsider S as Subset of BinFinTrees IndexedREAL by TARSKI:def 3;
consider x be element such that
A1: x in SOURCE by XBOOLE_0:def 1;
reconsider x as Element of SOURCE by A1;
A2: fcs.x in NAT by TARSKI:def 3;
A3:[ fcs.x, p.{x} ] in [:NAT,REAL:] by A2,ZFMISC_1:87;
set T = root-tree [ fcs.x, p.{x} ];
dom T = elementary_tree 0 by TREES_4:3;
then T is Element of FinTrees IndexedREAL by A3,TREES_3:def 8; then
A4: T in S;
for z be element st z in S holds z in
Funcs(elementary_tree 0,[:Seg (card SOURCE),rng p:])
proof
let z be element;
assume z in S; then
consider T be Element of FinTrees IndexedREAL such that
A5: z= T & T is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st T = root-tree [ fcs.x, p.{x} ];
consider x be Element of SOURCE such that
A6: T = root-tree [ fcs.x, p.{x} ] by A5;
A7: dom T = elementary_tree 0 by A5,FUNCT_2:def 1;
A8: rng T = {[ fcs.x, p.{x} ]} by A6,FUNCOP_1:8;
{x} in bool SOURCE; then
{x} in dom p by FUNCT_2:def 1; then
p.{x} in rng p by FUNCT_1:3; then
rng T c= [:Seg (card SOURCE),rng p:] by A8,ZFMISC_1:31,ZFMISC_1:87;
hence z in Funcs(elementary_tree 0,[:Seg (card SOURCE),rng p:])
by A5,A7,FUNCT_2:def 2;
end; then
S c= Funcs(elementary_tree 0,[:Seg (card SOURCE),rng p:]) by TARSKI:def 3;
hence thesis by A4;
end;
end;
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 be element st x in NAT & y in REAL & p.{} = [x,y] by ZFMISC_1:def 2;
func Vrootr p -> Real equals
(p.{}) `2;
correctness by A1;
func Vrootl p -> Nat equals
(p.{}) `1;
correctness by A1;
end;
definition
let T be finite binary DecoratedTree of IndexedREAL;
let p be Element of dom T;
func Vtree (p) -> Real equals
(T.p) `2;
correctness
proof
ex x,y be element st x in NAT & y in REAL & T.p = [x,y] by ZFMISC_1:def 2;
hence thesis;
end;
end;
definition
let p,q be finite binary DecoratedTree of IndexedREAL;
let k be Nat;
func MakeTree (p,q,k) -> finite binary DecoratedTree of IndexedREAL equals
[k,(Vrootr p) +(Vrootr q)] -tree (p,q);
correctness
proof
A1: k in NAT by ORDINAL1:def 12;
(Vrootr p) +(Vrootr q) in REAL by XREAL_0:def 1; then
[k,(Vrootr p) +(Vrootr q)] in [:NAT,REAL:] by A1,ZFMISC_1:87;
hence thesis;
end;
end;
definition
let X be non empty finite Subset of BinFinTrees IndexedREAL;
func MaxVl(X) -> Nat means
:Def9:
ex L be non empty finite Subset of NAT
st L = {Vrootl p where p is Element of BinFinTrees IndexedREAL: p in X }
& it = max L;
existence
proof
set L = {Vrootl p where p is Element of BinFinTrees IndexedREAL: p in X };
A1: X is finite;
A2: L is finite from FRAENKEL:sch 21 (A1);
consider q be element such that
A3: q in X by XBOOLE_0:def 1;
reconsider q as Element of BinFinTrees IndexedREAL by A3;
A4:Vrootl q in L by A3;
now let x be element;
assume x in L; then
consider p be Element of BinFinTrees IndexedREAL such that
A5: x= Vrootl p & p in X;
reconsider p as DecoratedTree of IndexedREAL;
dom p is finite & p is binary by Def2; then
reconsider p as finite binary DecoratedTree of IndexedREAL by FINSET_1:10;
thus x in NAT by A5,ORDINAL1:def 12;
end;
then reconsider L as non empty finite Subset of NAT by A2,A4,TARSKI:def 3;
take max L;
thus thesis;
end;
uniqueness;
end;
theorem
for X be non empty finite Subset of BinFinTrees IndexedREAL,
w be finite binary DecoratedTree of IndexedREAL st X = {w}
holds MaxVl X = Vrootl w
proof
let X be non empty finite Subset of BinFinTrees IndexedREAL,
w be finite binary DecoratedTree of IndexedREAL;
assume A1:X ={w};
consider L be non empty finite Subset of NAT such that A2:
L = {Vrootl p where p is Element of BinFinTrees IndexedREAL: p in X }
& MaxVl X = max L by Def9;
A3:for n be element st n in L holds n = Vrootl w
proof
let n be element;
assume n in L;
then ex p be Element of BinFinTrees IndexedREAL st n = Vrootl p &
p in X by A2;
hence thesis by TARSKI:def 1,A1;
end;
for n be element st n = Vrootl w holds n in L
proof
let n be element;
assume A4: n = Vrootl w;
consider y be element such that
A5: y in L by XBOOLE_0:def 1;
ex p be Element of BinFinTrees IndexedREAL st y = Vrootl p &
p in X by A2,A5;
hence thesis by A5,A4,TARSKI:def 1,A1;
end; then
L = {Vrootl w} by TARSKI:def 1,A3;
hence thesis by A2,XXREAL_2:11;
end;
theorem Th2:
for X,Y,Z be non empty finite Subset of BinFinTrees IndexedREAL
st Z = X \/ Y holds
MaxVl(Z) = max (MaxVl(X), MaxVl(Y))
proof
let X,Y,Z be non empty finite Subset of BinFinTrees IndexedREAL;
assume A1: Z = X \/ Y;
set mz = MaxVl(Z);
consider L be non empty finite Subset of NAT such that A2:
L = {Vrootl p where p is Element of BinFinTrees IndexedREAL: p in Z }
& MaxVl Z = max L by Def9;
mz in L & for b be Nat st b in L holds b <= mz by XXREAL_2:def 8,A2;then
consider p be Element of BinFinTrees IndexedREAL
such that A3: mz = Vrootl p & p in Z by A2;
consider LX be non empty finite Subset of NAT such that A4:
LX = {Vrootl p where p
is Element of BinFinTrees IndexedREAL: p in X }
& MaxVl X = max LX by Def9;
max LX in LX & for x be Nat st x in LX holds x <= max LX by XXREAL_2:def 8;
then consider px be Element of BinFinTrees IndexedREAL such that
A5: max LX = Vrootl px & px in X by A4;
px in Z by A5,A1,XBOOLE_0:def 3;then
Vrootl px in L by A2;then
A6: max LX <= mz by A5,XXREAL_2:def 8,A2;
consider LY be non empty finite Subset of NAT such that A7:
LY = {Vrootl p where p is Element of BinFinTrees IndexedREAL: p in Y }
& MaxVl Y = max LY by Def9;
max LY in LY & for y be Nat st y in LY holds y <= max LY
by XXREAL_2:def 8; then
consider py be Element of BinFinTrees IndexedREAL such that
A8: max LY = Vrootl py & py in Y by A7;
py in Z by A8,A1,XBOOLE_0:def 3; then
Vrootl py in L by A2;then
A9: max LY <= mz by A8,XXREAL_2:def 8,A2;
per cases by XBOOLE_0:def 3,A3,A1;
suppose p in X;then
Vrootl p in LX by A4;then
mz <= max LX by XXREAL_2:def 8,A3;then
mz = max LX by A6,XXREAL_0:1;
hence thesis by A4,A7,A9,XXREAL_0:def 10;
end;
suppose p in Y;then
Vrootl p in LY by A7;then
mz <= max LY by XXREAL_2:def 8,A3;then
mz = max LY by A9,XXREAL_0:1;
hence thesis by A4,A7,A6,XXREAL_0:def 10;
end;
end;
theorem
for X,Z be non empty finite Subset of BinFinTrees IndexedREAL
for Y be set st Z = X \ Y holds MaxVl(Z) <= MaxVl(X)
proof
let X,Z be non empty finite Subset of BinFinTrees IndexedREAL;
let Y be set;
assume A1:Z = X \ Y;
per cases;
suppose X misses Y;
hence thesis by XBOOLE_1:83,A1;
end;
suppose X meets Y;
A2:X = Z \/ (X \ Z) by XBOOLE_1:45,A1,XBOOLE_1:36;
per cases;
suppose X=Z; hence thesis; end;
suppose X <> Z;then
Z c< X by A1,XBOOLE_1:36,XBOOLE_0:def 8;then
reconsider W = X \ Z as non empty
finite Subset of BinFinTrees IndexedREAL by XBOOLE_1:105;
MaxVl(X) = max (MaxVl(Z), MaxVl(W)) by Th2,A2;
hence thesis by XXREAL_0:25;
end;
end;
end;
theorem
for X be non empty finite Subset of BinFinTrees IndexedREAL,
p be Element of BinFinTrees IndexedREAL
st p in X holds Vrootl p <= MaxVl(X)
proof
let X be non empty finite Subset of BinFinTrees IndexedREAL,
p be Element of BinFinTrees IndexedREAL;
assume A1: p in X;
consider L be non empty finite Subset of NAT such that A2:
L = {Vrootl p where p is Element of BinFinTrees IndexedREAL: p in X }
& MaxVl X = max L by Def9;
Vrootl p in L by A2,A1;
hence thesis by XXREAL_2:def 8,A2;
end;
defpred R[non empty finite Subset of BinFinTrees IndexedREAL,
finite binary DecoratedTree of IndexedREAL] means
$2 in $1 & for q be finite binary DecoratedTree of IndexedREAL
st q in $1 holds Vrootr $2 <= Vrootr q;
definition
let X be non empty finite Subset of BinFinTrees IndexedREAL;
mode MinValueTree of X -> finite binary DecoratedTree of IndexedREAL means
:Def10:
it in X & for q be finite binary DecoratedTree of IndexedREAL
st q in X holds Vrootr it <= Vrootr q;
existence
proof
defpred P[Nat] means
for X be non empty finite Subset of BinFinTrees IndexedREAL
st card (X) = $1
ex r be finite binary DecoratedTree of IndexedREAL st R[X,r];
A1:P[0];
A2:for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A3: P[n];
let X be non empty finite Subset of BinFinTrees IndexedREAL;
assume A4: card (X) = n+1;
consider p be element such that
A5: p in X by XBOOLE_0:def 1;
reconsider p as DecoratedTree of IndexedREAL by A5;
A6: dom p is finite & p is binary by A5,Def2;
reconsider p as finite binary DecoratedTree of IndexedREAL by A6,FINSET_1:10;
per cases;
suppose n=0; then
consider d be element such that
A7: X = {d} by CARD_2:42,A4;
X ={p} by A5,A7,TARSKI:def 1;
then R[X,p] by TARSKI:def 1;
hence thesis;
end;
suppose A8: n<> 0;
set Y = X \ {p};
A9: card {p} = 1 by CARD_2:42;
A10: card (Y) = card X - card {p} by ZFMISC_1:31,A5,CARD_2:44
.= n by A9,A4;
A11: Y c= X by XBOOLE_1:36;
reconsider Y as non empty finite Subset of BinFinTrees IndexedREAL by A10,A8;
A12: X = Y \/ {p} by XBOOLE_1:45,ZFMISC_1:31,A5;
consider q be finite binary DecoratedTree of IndexedREAL such that
A13: R[Y,q] by A10,A3;
per cases;
suppose A14: Vrootr p <= Vrootr q;
take r=p;
for t be finite binary DecoratedTree of IndexedREAL
st t in X holds Vrootr r <= Vrootr t
proof
let t be finite binary DecoratedTree of IndexedREAL;
assume t in X; then
A15: t in Y or t in {p} by XBOOLE_0:def 3,A12;
per cases by A15,TARSKI:def 1;
suppose t in Y;
then Vrootr q <= Vrootr t by A13;
hence Vrootr r <= Vrootr t by A14,XXREAL_0:2;
end;
suppose t = p;
hence Vrootr r <= Vrootr t;
end;
end;
hence thesis by A5;
end;
suppose A16: not Vrootr p <= Vrootr q;
take r = q;
for t be finite binary DecoratedTree of IndexedREAL
st t in X holds Vrootr r <= Vrootr t
proof
let t be finite binary DecoratedTree of IndexedREAL;
assume A17: t in X;
per cases by A17,A12,XBOOLE_0:def 3;
suppose t in Y;
hence Vrootr r <= Vrootr t by A13;
end;
suppose t in {p};
hence Vrootr r <= Vrootr t by A16,TARSKI:def 1;
end;
end;
hence thesis by A11,A13;
end;
end;
end;
A18: for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
card (X) is Nat;
hence thesis by A18;
end;
end;
Lm1:
for X be set,x be element
st ex u,v be element st u <> v & u in X & v in X holds
X \ {x} <> {}
proof
let X be set,x be element;
assume A1:
ex u,v be element st u <> v & u in X & v in X;
assume
A2: not X \ {x} <> {};
A3: now let z be element;
assume A4: z in X;
(not z in X) or z in {x} by XBOOLE_0:def 5,A2;
hence z=x by TARSKI:def 1,A4;
end;
consider u,v be element such that
A5: u <> v & u in X & v in X by A1;
u=x & v=x by A5,A3;
hence contradiction by A5;
end;
Lm2:
for X,Y be set, t,s,z be element
st X c= Y & t in Y & s in Y & z in Y holds
X \ {t,s} \/ {z} c= Y
proof
let X,Y be set, t,s,z be element;
assume A1: X c= Y & t in Y & s in Y & z in Y;
A2: X \ {t,s} c= Y by A1,XBOOLE_1:1;
{z} c= Y by ZFMISC_1:31,A1;
hence X \ {t,s} \/ {z} c= Y by A2,XBOOLE_1:8;
end;
Lm3:
for X be finite set st 2 <= card X holds
ex u,v be element st u <> v & u in X & v in X
proof
let X be finite set;
assume A1: 2 <= card X;
assume A2: not ex u,v be element st u <> v & u in X & v in X;
X <> {} by A1; then
consider z be element such that A3: z in X by XBOOLE_0:def 1;
A4: {z} c= X by ZFMISC_1:31,A3;
now let x be element;
assume x in X;
then x=z by A2,A3;
hence x in {z} by TARSKI:def 1;
end;
then X c= {z} by TARSKI:def 3;
then X = {z} by A4,XBOOLE_0:def 10;
then card X = 1 by CARD_1:30;
hence contradiction by A1;
end;
Lm4:
for X be finite set st 1 = card X holds ex u be element st X = {u}
proof
let X be finite set;
assume 1 = card X; then
card X = card {0} by CARD_1:30;
hence ex u be element st X = {u} by CARD_1:29;
end;
Lm5:
for X be finite set, t,s,z be element
st t in X & s in X & t <> s & not z in X holds
card (X \ {t,s} \/ {z}) = card X - 1
proof
let X be finite set, t,s,z be element;
assume A1: t in X & s in X & t <> s & not z in X;
A2: X = (X \ {t,s} ) \/ {t,s} by XBOOLE_1:45,ZFMISC_1:32,A1;
A3:card X = card (X \ {t,s} ) + card ({t,s}) by XBOOLE_1:79,A2,CARD_2:40
.= card (X \ {t,s} ) + 2 by CARD_2:57,A1;
X misses {z} by A1,ZFMISC_1:50;
hence card (X \ {t,s} \/ {z}) = card (X \ {t,s} )
+ card ({z}) by CARD_2:40,XBOOLE_1:63
.= (card X - 2) + 1 by CARD_1:30,A3
.= card X -1;
end;
theorem Th5:
card (Initial-Trees(p)) = card SOURCE
proof
set L = {T where T is Element of FinTrees IndexedREAL :
T is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st
T = root-tree [ (canFS SOURCE)".x, p.{x} ] };
reconsider fcs = (canFS SOURCE)" as Function of SOURCE, Seg (card SOURCE)
by FINSEQ_1:95;
len canFS SOURCE = card SOURCE by FINSEQ_1:93; then
dom (canFS SOURCE) = Seg (card SOURCE)
& rng (canFS SOURCE) = SOURCE by FINSEQ_1:def 3,FUNCT_2:def 3; then
reconsider g = canFS SOURCE
as Function of Seg (card SOURCE),SOURCE by FUNCT_2:1;
defpred P[element,element] means $2= root-tree [ fcs.$1, p.{$1} ];
A1: for x being element st x in SOURCE
ex y being element st y in Initial-Trees(p) & P[x,y]
proof
let x be element;
assume
A2: x in SOURCE;
then reconsider x0=x as Element of SOURCE;
A3: fcs.x in Seg card SOURCE by A2,FUNCT_2:5;
p.{x0} in REAL; then
A4: [ fcs.x, p.{x} ] in [:NAT,REAL:] by A3,ZFMISC_1:87;
take T = root-tree [ fcs.x, p.{x} ];
dom T = elementary_tree 0 by TREES_4:3;
then T is Element of FinTrees IndexedREAL by A4,TREES_3:def 8;
hence thesis by A4,A2;
end;
consider f being Function of SOURCE,Initial-Trees(p) such that
A5: for x being element st x in SOURCE holds P[x,f.x]
from FUNCT_2:sch 1(A1);
now let x1,x2 be element;
assume A6: x1 in dom f & x2 in dom f & f.x1=f.x2; then
A7: x1 in SOURCE & x2 in SOURCE;
A8: f.x1= root-tree [ fcs.x1, p.{x1} ] by A5,A6;
A9: f.x2= root-tree [ fcs.x2, p.{x2} ] by A5,A6;
A10:f.x1 in Initial-Trees(p) by A6,FUNCT_2:5;
then reconsider T1=f.x1 as DecoratedTree of IndexedREAL;
A11: dom T1 is finite & T1 is binary by A10,Def2;
reconsider T1 as finite binary DecoratedTree of IndexedREAL
by A11,FINSET_1:10;
A12: f.x2 in Initial-Trees(p) by A6,FUNCT_2:5; then
reconsider T2=f.x2 as DecoratedTree of IndexedREAL;
A13: dom T2 is finite & T2 is binary by A12,Def2;
reconsider T2 as finite binary
DecoratedTree of IndexedREAL by A13,FINSET_1:10;
A14: {} in elementary_tree 0 by TARSKI:def 1,TREES_1:29; then
A15: T1.{} = [ fcs.x1, p.{x1} ] by A8,FUNCOP_1:7;
A16:fcs.x1 = ([ fcs.x1, p.{x1} ])`1
.= ([ fcs.x2, p.{x2} ])`1 by A15,A6,A9,A14,FUNCOP_1:7
.= fcs.x2;
x1 in dom fcs & x2 in dom fcs by A7,FUNCT_2:def 1;
hence x1=x2 by A16,FUNCT_1:def 4;
end; then
A17: f is one-to-one by FUNCT_1:def 4;
now let z be element;
assume z in Initial-Trees(p); then
consider T be Element of FinTrees IndexedREAL such that
A18:z= T & T is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st T = root-tree [ (canFS SOURCE)".x, p.{x} ];
consider x be Element of SOURCE such that
A19: T = root-tree [ (canFS SOURCE)".x, p.{x} ] by A18;
z = f.x by A19,A18,A5;
hence z in rng f by FUNCT_2:112;
end;
then Initial-Trees(p) c= rng f by TARSKI:def 3; then
A20: Initial-Trees(p) = rng f by XBOOLE_0:def 10;
dom f = SOURCE by FUNCT_2:def 1;
hence thesis by CARD_1:5,A17,WELLORD2:def 4,A20;
end;
theorem Th6:
for X be non empty finite Subset of BinFinTrees IndexedREAL,
s,t be finite binary DecoratedTree of IndexedREAL holds
not MakeTree (t,s,(MaxVl(X) + 1)) in X
proof
let X be non empty finite Subset of BinFinTrees IndexedREAL,
s,t be finite binary DecoratedTree of IndexedREAL;
assume A1:MakeTree (t,s,(MaxVl(X) + 1)) in X;
set px = MakeTree (t,s,(MaxVl(X) + 1));
consider L be non empty finite Subset of NAT such that
A2: L = {Vrootl p where p
is Element of BinFinTrees IndexedREAL: p in X }
& MaxVl(X) = max L by Def9;
dom px is finite & dom px is binary by BINTREE1:def 3; then
reconsider px as Element of BinFinTrees IndexedREAL by Def2;
Vrootl px in L by A1,A2; then
A3: Vrootl px <= MaxVl(X) by A2,XXREAL_2:def 8;
px.{} = [(MaxVl(X) + 1),(Vrootr t) +(Vrootr s)] by TREES_4:def 4;
hence contradiction by NAT_1:13,A3;
end;
definition
let X be set;
func LeavesSet(X) -> Subset of bool IndexedREAL equals
{ Leaves p where p is Element of BinFinTrees IndexedREAL : p in X};
correctness
proof
set L = { Leaves p where p is Element of BinFinTrees IndexedREAL : p in X};
now let x be element;
assume x in L; then
consider p be Element of BinFinTrees IndexedREAL such that
A1: Leaves p =x & p in X;
thus x in bool IndexedREAL by A1;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th7:
for X be finite binary DecoratedTree of IndexedREAL
holds LeavesSet({X}) = {Leaves X}
proof
let X be finite binary DecoratedTree of IndexedREAL;
for x be element holds x in LeavesSet({X}) iff x in {Leaves X}
proof
let x be element;
hereby assume x in LeavesSet({X}); then
consider p be Element of BinFinTrees IndexedREAL such that
A1: x = Leaves p & p in {X};
p = X by A1,TARSKI:def 1;
hence x in {Leaves X} by TARSKI:def 1,A1;
end;
assume x in {Leaves X}; then
A2: x = Leaves X by TARSKI:def 1;
dom X is finite & dom X is binary by BINTREE1:def 3; then
reconsider p= X as Element of BinFinTrees IndexedREAL by Def2;
p in {X} by TARSKI:def 1;
hence x in LeavesSet({X}) by A2;
end;
hence thesis by TARSKI:2;
end;
theorem Th8:
for X,Y be set
holds LeavesSet(X \/ Y ) = LeavesSet(X) \/ LeavesSet(Y)
proof
let X,Y be set;
for x be element
holds x in LeavesSet(X \/ Y) iff x in LeavesSet(X) \/ LeavesSet(Y)
proof
let x be element;
hereby assume x in LeavesSet(X \/ Y); then
consider p be Element of BinFinTrees IndexedREAL such that
A1: x = Leaves p & p in X \/ Y;
p in X or p in Y by A1,XBOOLE_0:def 3;
then x in LeavesSet(X) or x in LeavesSet(Y) by A1;
hence x in LeavesSet(X) \/ LeavesSet(Y) by XBOOLE_0:def 3;
end;
assume A2: x in LeavesSet(X) \/ LeavesSet(Y);
per cases by A2,XBOOLE_0:def 3;
suppose x in LeavesSet(X); then
consider p be Element of BinFinTrees IndexedREAL such that
A3: x = Leaves p & p in X;
p in X \/ Y by TARSKI:def 3,XBOOLE_1:7,A3;
hence x in LeavesSet(X \/ Y) by A3;
end;
suppose x in LeavesSet(Y); then
consider p be Element of BinFinTrees IndexedREAL such that
A4: x = Leaves p & p in Y;
p in X \/ Y by TARSKI:def 3,XBOOLE_1:7,A4;
hence x in LeavesSet(X \/ Y) by A4;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th9:
for s,t be Tree holds not {} in Leaves (tree (t,s))
proof
let s,t be Tree;
assume A1: {} in Leaves (tree (t,s));
set q = <*t,s*>;
q.1 = t by FINSEQ_1:44; then
0 < len q & {} in q . (0 + 1) by TREES_1:22; then
<* 0 *>^{} in tree(t,s) by TREES_3:def 15; then
A2: <* 0 *> in tree(t,s) by FINSEQ_1:34;
for p be element holds p in tree (t,s) iff p in elementary_tree 0
proof
let p0 be element;
hereby assume that
A3: p0 in tree (t,s) and
A4: not p0 in elementary_tree 0;
reconsider p=p0 as FinSequence of NAT by A3,TREES_1:19;
p <> {} by A4, TARSKI:def 1, TREES_1:29;
then consider q being FinSequence of NAT, n being Element of NAT such that
A5: p = <*n*> ^ q by FINSEQ_2:130;
{} ^ <*n*> = <*n*> by FINSEQ_1:34;
hence contradiction by A1,TREES_1:55,A3, A5, TREES_1:21;
end;
assume p0 in elementary_tree 0;
then p0 = {} by TARSKI:def 1, TREES_1:29;
hence p0 in tree (t,s) by TREES_1:22;
end;
then <* 0 *> in elementary_tree 0 by A2;
hence contradiction by TARSKI:def 1,TREES_1:29;
end;
theorem Th10:
for s,t be 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
let s,t be Tree;
set L = {<* 0 *>^p where p is Element of t:p in Leaves t };
set R = {<*1*>^p where p is Element of s:p in Leaves s };
set H = Leaves tree(t,s);
set q = <*t,s*>;
A1: len q = 2 by FINSEQ_1:44;
A2: q.1 = t by FINSEQ_1:44;
A3: q.2 = s by FINSEQ_1:44;
for x be element holds x in H iff x in L \/ R
proof
let x be element;
hereby assume A4: x in H; then
x = {} or ex n being Nat, r being FinSequence st
( n < len q & r in q . (n + 1) & x = <*n*> ^ r ) by TREES_3:def 15; then
consider n being Nat, r being FinSequence such that
A5: n < len q & r in q . (n + 1) & x = <*n*> ^ r by A4,Th9;
per cases by NAT_1:23,A1,A5;
suppose A6: n = 0; then
r in Leaves t by BINTREE1:6,A4,A2,A5; then
x in L by A6,A5;
hence x in L \/ R by XBOOLE_0:def 3;
end;
suppose A7:n = 1;
then r in Leaves s by BINTREE1:6,A4,A5,A3;
then x in R by A7,A5;
hence x in L \/ R by XBOOLE_0:def 3;
end;
end;
assume
A8: x in L \/ R;
per cases by A8,XBOOLE_0:def 3;
suppose x in L; then
consider p be Element of t
such that A9: x = <* 0 *>^p & p in Leaves t;
0 < len q & p in q . (0 + 1) by A2; then
x in tree(t,s) by A9,TREES_3:def 15;
hence x in H by BINTREE1:6,A9;
end;
suppose x in R; then
consider p be Element of s such that A10: x = <* 1 *>^p & p in Leaves s;
1 < len q & p in q . (1 + 1) by A1,A3; then
x in tree(t,s) by A10,TREES_3:def 15;
hence x in H by BINTREE1:6,A10;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th11:
for s,t be DecoratedTree, x be element,
q being FinSequence of NAT st q in dom t holds
(x-tree (t,s)). (<* 0 *>^q) = t.q
proof
let s,t be DecoratedTree, x be element, q be FinSequence of NAT;
assume A1: q in dom t;
set r = <*t, s*>;
0 < len r; then
A2: (x-tree (t,s)) | <* 0 *> = r . (0 + 1) by TREES_4:def 4
.= t by FINSEQ_1:44;
dom ( (x-tree (t,s)) | <* 0 *> ) = dom (x-tree (t,s)) | <* 0 *>
by TREES_2:def 10;
hence thesis by A1,A2,TREES_2:def 10;
end;
theorem Th12:
for s,t be DecoratedTree, x be element,
q being FinSequence of NAT st q in dom s holds
(x-tree (t,s)). (<* 1 *>^q) = s.q
proof
let s,t be DecoratedTree, x be element,
q being FinSequence of NAT;
assume A1: q in dom s;
set r = <*t, s*>;
A2: len r = 2 by FINSEQ_1:44;
A3: (x-tree (t,s)) | <* 1 *> = r . (1 + 1) by A2,TREES_4:def 4
.= s by FINSEQ_1:44;
dom ( (x-tree (t,s)) | <* 1 *> ) = dom (x-tree (t,s)) | <* 1 *>
by TREES_2:def 10;
hence thesis by A1,A3,TREES_2:def 10;
end;
theorem Th13:
for s,t be DecoratedTree, x be element holds
Leaves (x-tree (t,s)) = (Leaves t) \/ Leaves s
proof
let s,t be DecoratedTree, x be element;
set q = <*dom t,dom s*>;
A1: len q = 2 by FINSEQ_1:44;
A2: q.1 = dom t by FINSEQ_1:44;
A3: q.2 = dom s by FINSEQ_1:44;
A4: dom (x -tree (t,s)) = tree ((dom t),(dom s)) by TREES_4:14;
A5: Leaves (tree ((dom t),(dom s))) =
{<* 0 *>^p where p is Element of (dom t) : p in Leaves (dom t)}
\/ {<* 1 *>^p where p is Element of (dom s)
: p in Leaves (dom s)} by Th10;
set L = {<* 0 *>^p where p is Element of (dom t) : p in Leaves (dom t) };
set R = {<* 1 *>^p where p is Element of (dom s) : p in Leaves (dom s) };
A6: Leaves (x-tree(t,s))
= ((x-tree(t,s)) .: L) \/ ((x-tree(t,s)) .: R) by RELAT_1:120,A5,A4;
for z be element holds
z in ((x-tree(t,s)) .: L) iff z in t .: (Leaves dom t)
proof
let z be element;
hereby assume z in ((x-tree(t,s)) .: L);
then consider q be element such that
A7: q in dom (x-tree(t,s)) & q in L & z = (x-tree(t,s)).q
by FUNCT_1:def 6;
consider p be Element of dom t such that
A8: q=<* 0 *>^p & p in Leaves dom t by A7;
z = t.p by A7,Th11,A8;
hence z in t .: (Leaves dom t) by A8,FUNCT_1:def 6;
end;
assume z in t .: (Leaves dom t); then
consider p0 being element such that
A9: p0 in dom t & p0 in Leaves dom t
& z = t.p0 by FUNCT_1:def 6;
reconsider p=p0 as Element of dom t by A9;
A10: (x-tree (t,s)). (<* 0 *>^p) = t.p by Th11;
0 < len q & p in q . (0 + 1) by A2; then
A11: (<* 0 *>^p) in dom (x -tree (t,s)) by TREES_3:def 15,A4;
(<* 0 *>^p) in L by A9;
hence z in ((x-tree(t,s)) .: L) by A10,A9,FUNCT_1:def 6,A11;
end;
then
A12: ((x-tree(t,s)) .: L) = t .: (Leaves (dom t )) by TARSKI:2;
for z be element holds
z in ((x-tree(t,s)) .: R) iff z in s .: (Leaves (dom s ))
proof
let z be element;
hereby assume z in ((x-tree(t,s)) .: R);
then consider q be element such that
A13: q in dom (x-tree(t,s)) & q in R & z = (x-tree(t,s)).q
by FUNCT_1:def 6;
consider p be Element of dom s such that
A14: q=<* 1 *>^p & p in Leaves dom s by A13;
(x-tree(t,s)).(<* 1 *>^p ) = s.p by Th12;
hence z in s .: (Leaves dom s) by A14,FUNCT_1:def 6,A13;
end;
assume z in s .: (Leaves dom s); then
consider p0 being element such that
A15: p0 in dom s & p0 in Leaves dom s
& z = s.p0 by FUNCT_1:def 6;
reconsider p=p0 as Element of dom s by A15;
A16: (x-tree (t,s)). (<* 1 *>^p) = s.p by Th12;
1 < len q & p in q . (1 + 1) by A1,A3; then
A17: (<* 1 *>^p) in dom (x -tree (t,s)) by TREES_3:def 15,A4;
(<* 1 *>^p) in R by A15;
hence z in ((x-tree(t,s)) .: R) by A16,A15,FUNCT_1:def 6,A17;
end;
hence thesis by A6,A12,TARSKI:2;
end;
theorem Th14:
for k be Nat
for s,t be finite binary DecoratedTree of IndexedREAL
holds union LeavesSet( {s,t} ) = union LeavesSet({MakeTree (t,s,k)})
proof
let k be Nat;
let s,t be finite binary DecoratedTree of IndexedREAL;
A1: {s} \/ {t} = union { {s},{t} } by ZFMISC_1:75
.= {s,t} by ZFMISC_1:26;
thus union LeavesSet( {s,t} )
= union (LeavesSet( {s}) \/ LeavesSet( {t}) ) by Th8,A1
.= union LeavesSet( {s} ) \/ union LeavesSet( {t} ) by ZFMISC_1:78
.= union { Leaves s } \/ union LeavesSet( {t} ) by Th7
.= union { Leaves s } \/ union {Leaves t} by Th7
.= (Leaves s) \/ union {Leaves t} by ZFMISC_1:25
.= (Leaves s) \/ (Leaves t) by ZFMISC_1:25
.= Leaves MakeTree (t,s,k) by Th13
.= union {Leaves MakeTree (t,s,k)} by ZFMISC_1:25
.= union LeavesSet({MakeTree (t,s,k)}) by Th7;
end;
theorem Th15:
Leaves (elementary_tree 0 ) = elementary_tree 0
proof
for x be element holds
x in Leaves (elementary_tree 0 ) iff x in elementary_tree 0
proof
let x be element;
thus x in Leaves (elementary_tree 0 ) implies x in elementary_tree 0;
assume x in elementary_tree 0; then
reconsider x0=x as Element of elementary_tree 0;
not x0 ^ <* 0 *> in elementary_tree 0 by TREES_1:29,TARSKI:def 1;
hence x in Leaves (elementary_tree 0 ) by TREES_1:54;
end;
hence thesis by TARSKI:2;
end;
theorem Th16:
for x be element, D be non empty set,
T be finite binary DecoratedTree of D st T = root-tree x holds
Leaves (T) = {x}
proof
let x be element, D be non empty set,
T be finite binary DecoratedTree of D;
assume A1: T = root-tree x;
A2: {} in elementary_tree 0 by TARSKI:def 1,TREES_1:29; then
A3: T.{} = x by A1,FUNCOP_1:7;
A4: dom T = elementary_tree 0 by FUNCT_2:def 1,A1;
A5: Leaves dom T = {{}} by TREES_1:29,Th15,FUNCT_2:def 1,A1;
thus Leaves (T) = Im (T,{}) by RELAT_1:def 16,A5
.={x} by A3,A4,A2,FUNCT_1:59;
end;
begin :: Binary Huffman Tree
definition
let SOURCE,p,Tseq,q;
pred Tseq,q,p is_constructingBinHuffmanTree means
:Def12:
Tseq.1 = Initial-Trees(p) &
len Tseq = card SOURCE &
( for i be Nat st 1<= i & i < len Tseq
ex X,Y being non empty finite Subset of BinFinTrees IndexedREAL,
s being MinValueTree of X,
t being MinValueTree of Y,
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 be finite binary DecoratedTree of IndexedREAL
st { T } = Tseq.(len Tseq)) &
dom q = Seg card SOURCE
& (for k be Nat st k in Seg card SOURCE
holds q.k = card(Tseq.k) & q.k <> 0)
& (for k be Nat holds (k < card SOURCE implies q.(k+1) = q.1 - k))
& (for k be Nat st 1<=k & k < card SOURCE holds 2 <= q.k);
end;
theorem Th17:
ex Tseq,q st Tseq,q,p is_constructingBinHuffmanTree
proof
defpred P1[Nat, set, set] means
((ex u,v be element st u <> v & u in $2 & v in $2) implies
ex 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 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 P1[n,x,y]
proof
let n be Nat;
assume 1 <= n & n < card (SOURCE);
let x be Element of (BoolBinFinTrees IndexedREAL);
now assume ex u,v be element st u <> v & u in x & v in x;
then consider u,v be element such that
A2: u <> v & u in x & v in x;
x in BoolBinFinTrees IndexedREAL; then
ex z be 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 \ {s};
reconsider Y as Subset of BinFinTrees IndexedREAL;
reconsider Y as non empty finite Subset of BinFinTrees IndexedREAL
by A2,Lm1;
set t = the MinValueTree of Y;
set w= MakeTree (t,s,MaxVl(X) + 1);
A3: w in {MakeTree (t,s,MaxVl(X) + 1),
MakeTree (s,t,MaxVl(X) + 1)} by TARSKI:def 2;
set y = (X \ {t,s} ) \/ {w};
A4: s in X & t in Y by Def10;
dom (MakeTree (t,s,MaxVl(X) + 1))
is finite & dom (MakeTree (t,s,MaxVl(X) + 1)) is binary &
dom (MakeTree (s,t,MaxVl(X) + 1))
is finite & dom (MakeTree (s,t,MaxVl(X) + 1)) is binary by BINTREE1:def 3;
then w in BinFinTrees IndexedREAL by Def2; then
y c= BinFinTrees IndexedREAL by A4,Lm2;
then y in (BoolBinFinTrees IndexedREAL);
hence ex y being Element of (BoolBinFinTrees IndexedREAL) st
ex X,Y be non empty finite Subset of BinFinTrees IndexedREAL,
s being MinValueTree of X,
t being MinValueTree of Y,
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;
end;
hence thesis;
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
P1[n,Tseq.n,Tseq.(n + 1)] ) from RECDEF_1:sch 4(A1);
defpred P2[element,element] means
ex X be finite set st Tseq.$1 = X & $2 = card X & $2 <> 0;
A6: for k be Nat st k in Seg card (SOURCE)
ex x being Element of NAT st P2[k,x]
proof
let k be Nat;
assume k in Seg card SOURCE; 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 be 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;
thus thesis by A7;
end;
consider q being FinSequence of NAT such that
A8: dom q = Seg card SOURCE
& for k be Nat st k in Seg card SOURCE holds P2[k,q.k]
from FINSEQ_1:sch 5(A6);
A9: for k be Nat st k in Seg card SOURCE
holds q.k = card(Tseq.k) & q.k <> 0
proof
let k be Nat;
assume k in Seg card (SOURCE); then
ex X be finite set st Tseq.k = X & q.k = card X & q.k <> 0 by A8;
hence q.k = card(Tseq.k) & q.k <> 0;
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 be Nat st 1<= k & k < card SOURCE holds
(2 <= q.k implies q.(k+1) = q.k - 1)
proof
let k be Nat;
assume A14: 1<= k & k < card (SOURCE);
thus 2 <= q.k implies q.(k+1) = q.k - 1
proof
assume A15: 2 <= q.k;
A16: (ex u,v be element st u <> v & u in Tseq.k & v in Tseq.k) implies
ex X,Y be non empty finite Subset of BinFinTrees IndexedREAL st
ex s being MinValueTree of X,
t being MinValueTree of Y,
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 be finite set such that
A20: Tseq.k = Tseqk & q.k = card Tseqk & q.k <> 0 by FINSEQ_1:1,A14,A8;
consider X,Y be 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;
end;
end;
defpred P4[Nat] means $1 < card SOURCE implies q.($1+1) = q.1 - $1;
A24: P4[0];
A25: for n be Nat st P4[n] holds P4[n+1]
proof
let n be Nat;
assume A26: P4[n];
assume A27: n+1 < card SOURCE;
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); 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;
end;
q.((n+1)+1) = q.(n+1) - 1 by A13,A30,A27,NAT_1:11;
hence thesis by A28,A26,A27,XXREAL_0:2;
end;
A31: for n be Nat holds P4[n] from NAT_1:sch 2(A24,A25);
A32: for n be Nat st 1<=n & n < card SOURCE holds 2 <= q.n
proof
let n be Nat;
assume A33: 1<=n & n < card SOURCE;
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;
end;
A35: for k be Nat st 1<= k & k < len Tseq holds
ex X,Y be non empty finite Subset of BinFinTrees IndexedREAL st
ex s being MinValueTree of X,
t being MinValueTree of Y,
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;
assume A36:1<= k & k < len Tseq;
A37: (ex u,v be element st u <> v & u in Tseq.k & v in Tseq.k) implies
ex X,Y be non empty finite Subset of BinFinTrees IndexedREAL st
ex s being MinValueTree of X,
t being MinValueTree of Y,
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 be finite set st Tseq.k = Tseqk & q.k = card Tseqk & q.k <> 0
by FINSEQ_1:1,A36,A5,A8;
hence thesis by A37,Lm3,A36,A32,A5;
end;
reconsider n1 = card (SOURCE) -1 as Nat by NAT_1:14,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 be 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 be element 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 as finite binary DecoratedTree of IndexedREAL
by A44,FINSET_1:10;
{T} = Tseq.( (len Tseq) ) by A40,A41,A5;
hence thesis by A35,A5,A8,A9,A31,A32,Def12;
end;
definition
let SOURCE,p;
mode BinHuffmanTree of p -> finite binary DecoratedTree of IndexedREAL means
:Def13:
ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL,
q being FinSequence of NAT
st Tseq,q,p is_constructingBinHuffmanTree &
{it} = Tseq.(len Tseq);
existence
proof
ex Tseq,q st Tseq,q,p is_constructingBinHuffmanTree by Th17;
hence thesis;
end;
end;
reserve T for BinHuffmanTree of p;
theorem Th18:
union LeavesSet(Initial-Trees p) = { z where z is Element of [:NAT,REAL:]
:ex x be Element of SOURCE st z =[(canFS SOURCE)".x,p.{x}] }
proof
set L = union LeavesSet(Initial-Trees(p));
set R = { z where z is Element of [:NAT,REAL:]
:ex x be Element of SOURCE st z =[(canFS SOURCE)".x,p.{x}] };
reconsider fcs = (canFS SOURCE)" as Function of SOURCE, Seg (card SOURCE)
by FINSEQ_1:95;
for x be element holds x in L iff x in R
proof
let x be element;
hereby assume x in L; then
consider Y be set
such that A1: x in Y & Y in LeavesSet(Initial-Trees(p)) by TARSKI:def 4;
consider q be Element of BinFinTrees IndexedREAL
such that A2: Y = Leaves q & q in Initial-Trees(p) by A1;
consider T be Element of FinTrees IndexedREAL such that
A3: q = T & T is finite binary DecoratedTree of IndexedREAL &
ex y be Element of SOURCE st
T = root-tree [ (canFS SOURCE)".y, p.{y} ] by A2;
reconsider T as finite binary DecoratedTree of IndexedREAL by A3;
consider y be Element of SOURCE such that
A4: T = root-tree [ (canFS SOURCE)".y, p.{y} ] by A3;
Y = {[ (canFS SOURCE)".y, p.{y} ]} by A2,A3,A4,Th16; then
x = [ (canFS SOURCE)".y, p.{y} ] by TARSKI:def 1,A1;
hence x in R by A1;
end;
assume x in R; then
consider z be Element of [:NAT,REAL:] such that
A5: x=z & ex y be Element of SOURCE
st z =[(canFS SOURCE)".y,p.{y}];
consider y be Element of SOURCE such that
A6: z =[(canFS SOURCE)".y,p.{y}] by A5;
fcs.y in NAT by TARSKI:def 3; then
A7: [ fcs.y, p.{y} ] in [:NAT,REAL:] by ZFMISC_1:87;
set T = root-tree [ fcs.y, p.{y} ];
A8: dom T = elementary_tree 0 by TREES_4:3;
then T is Element of FinTrees IndexedREAL by TREES_3:def 8,A7; then
A9: T in Initial-Trees(p);
reconsider T as Element of BinFinTrees IndexedREAL by A7,A8,Def2;
Leaves (T) = {[(canFS SOURCE)".y,p.{y}]} by Th16; then
A10: x in (Leaves T) by TARSKI:def 1,A5,A6;
(Leaves T) in LeavesSet(Initial-Trees(p)) by A9;
hence x in L by TARSKI:def 4,A10;
end;
hence thesis by TARSKI:2;
end;
theorem Th19:
Tseq,q,p is_constructingBinHuffmanTree implies
for i be Nat st 1 <= i & i <= len Tseq holds
union LeavesSet(Tseq.i) = { z where z is Element of [:NAT,REAL:]
:ex x be Element of SOURCE
st z =[(canFS SOURCE)".x,p.{x}] }
proof
assume A1: Tseq,q,p is_constructingBinHuffmanTree;
defpred P[Nat] means $1 < len Tseq implies
union LeavesSet(Tseq.($1+1)) = { z where z is Element of [:NAT,REAL:]
:ex x be Element of SOURCE st z =[(canFS SOURCE)".x,p.{x}] };
A2:P[0] by Th18,A1;
A3:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A4: P[k];
assume
A5: k+1 < len Tseq;
A6: k<=k+1 by NAT_1:11;
consider X,Y be 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 be 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;
end;
A13:for k be Nat holds P[k] from NAT_1:sch 2(A2,A3);
let i be Nat;
assume A14: 1 <= i & i <= len Tseq; 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 be Element of SOURCE st z =[(canFS SOURCE)".x,p.{x}] } by A13;
hence thesis;
end;
theorem
Leaves T ={ z where z is Element of [:NAT,REAL:]
:ex x be Element of SOURCE
st z =[(canFS SOURCE)".x,p.{x}] }
proof
consider Tseq be FinSequence of BoolBinFinTrees IndexedREAL,
q being FinSequence of NAT such that
A1: Tseq,q,p is_constructingBinHuffmanTree &
{T} = Tseq.(len Tseq) by Def13;
1 <= len Tseq by NAT_1:14,A1; then
A2: union LeavesSet({T}) = { z where z is Element of [:NAT,REAL:]
:ex x be Element of SOURCE st z =[(canFS SOURCE)".x,p.{x}] } by Th19,A1;
LeavesSet({T}) = {Leaves T } by Th7;
hence thesis by A2,ZFMISC_1:25;
end;
theorem Th21:
Tseq,q,p is_constructingBinHuffmanTree implies
for i be Nat
for T be finite binary DecoratedTree of IndexedREAL
for t,s,r be 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
assume A1:Tseq,q,p is_constructingBinHuffmanTree;
defpred P[Nat] means 1 <=$1 & $1 <=len Tseq implies
for T be finite binary DecoratedTree of IndexedREAL
for a,b,c be Element of dom T
st T in Tseq.$1 & a in ( dom T \ (Leaves dom T) )
& b = (a^<* 0 *> ) & c = (a^<* 1 *> )
holds Vtree (a) = Vtree (b) + Vtree (c);
A2: P[0];
A3: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A4: P[i];
assume A5: 1 <=i+1 & i+1 <=len Tseq;
let d be finite binary DecoratedTree of IndexedREAL;
let a,b,c be Element of dom d;
assume A6: d in Tseq.(i+1) & a in ( dom d \ (Leaves dom d) )
& b = (a^<* 0 *> ) & c = (a^<* 1 *> );
per cases;
suppose i = 0; then
consider d0 be Element of FinTrees IndexedREAL such that
A7: d0=d & d0 is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st
d0 = root-tree [ (canFS SOURCE)".x, p.{x} ] by A1,A6;
dom d = elementary_tree 0 by A7,FUNCT_2:def 1;
hence Vtree (a) = Vtree (b) + Vtree (c) by A6,XBOOLE_1:37,Th15;
end;
suppose A8:i <> 0; then
1<= i & i < len Tseq by A5,XXREAL_0:2,NAT_1:16,NAT_1:14;
then consider X,Y be 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
A9: 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;
A10: s in X & t in Y by Def10;
A11: w = MakeTree (t,s,MaxVl(X) + 1) or
w = MakeTree (s,t,MaxVl(X) + 1) by A9,TARSKI:def 2;
per cases by XBOOLE_0:def 3,A9,A6;
suppose d in (X \ {t,s} );
then d in Tseq.i by A9,XBOOLE_0:def 5;
hence Vtree (a) = Vtree (b) + Vtree (c) by
A8,A5,XXREAL_0:2,NAT_1:16,NAT_1:14,A4,A6;
end;
suppose A12:d in {w};
per cases by A12,TARSKI:def 1,A11;
suppose A13:
d = [MaxVl(X) + 1,(Vrootr t) +(Vrootr s)] -tree (t,s);
set bx = [MaxVl(X) + 1,(Vrootr t) +(Vrootr s)];
set q = <*dom t, dom s*>;
A14: len q = 2 by FINSEQ_1:44;
A15: dom (bx -tree (t,s)) = tree ((dom t),(dom s)) by TREES_4:14;
per cases by A15,A13,TREES_3:def 15;
suppose A16: a = {};
A17:Vtree (a) = ( [MaxVl(X) + 1,(Vrootr t) +(Vrootr s)] )`2
by TREES_4:def 4,A13,A16
.= (Vrootr t) +(Vrootr s);
A18: {} in dom t by TREES_1:22;
A19: d.<* 0 *> = d.(<* 0 *>^(<*> NAT) ) by FINSEQ_1:34
.=t.(<*> NAT) by A18,A13,Th11;
A20: Vtree (b) = (Vrootr t) by A16,FINSEQ_1:34,A6,A19;
A21: {} in dom s by TREES_1:22;
d.<* 1 *> = d.(<* 1 *>^(<*> NAT) ) by FINSEQ_1:34
.=s.(<*> NAT) by A21,A13,Th12;
hence Vtree (a) = Vtree (b) + Vtree (c) by A17,A20,A16,FINSEQ_1:34,A6;
end;
suppose ex n being Nat, f being FinSequence st
( n < len q & f in q . (n + 1) & a = <*n*> ^ f );
then consider n being Nat, f being FinSequence such that
A22: n < len q & f in q . (n + 1) & a = <*n*> ^ f;
per cases by NAT_1:23,A22,A14;
suppose A23:n = 0; then
reconsider f as Element of dom t by A22,FINSEQ_1:44;
A24:Vtree (a) = Vtree (f) by A13,A23,Th11,A22;
not a in Leaves dom d by A6,XBOOLE_0:def 5; then
A25: not f in Leaves dom t by A23,BINTREE1:6,A15,A13,A22; then
A26: f in ( dom t \ (Leaves dom t) ) by XBOOLE_0:def 5;
A27: t in Tseq.i by A10,A9,XBOOLE_0:def 5;
dom t is binary by BINTREE1:def 3;
then A28: succ f = { ( f ^ <* 0 *> ),(f ^ <*1*> ) } by A25;
(f ^ <* 0 *>) in {(f ^ <* 0 *>),(f ^ <*1*>)} by TARSKI:def 2; then
reconsider b1 = (f^<* 0 *> ) as Element of dom t by A28;
(f ^ <* 1 *>) in {(f ^ <* 0 *>),(f ^ <*1*>)} by TARSKI:def 2; then
reconsider c1 = (f^<* 1 *> ) as Element of dom t by A28;
A29: Vtree (f) = Vtree (b1) + Vtree (c1)
by A8,A4,A5,XXREAL_0:2,NAT_1:16,NAT_1:14,A26,A27;
A30: b = <* 0 *> ^b1 by FINSEQ_1:32,A6,A23,A22;
A31: Vtree (b) = Vtree (b1) by A13,A30,Th11;
c = <* 0 *> ^c1 by FINSEQ_1:32,A6,A23,A22;
hence Vtree (a) = Vtree (b) + Vtree (c) by A24,A29,A31,A13,Th11;
end;
suppose A32:n = 1; then
reconsider f as Element of dom s by A22,FINSEQ_1:44;
not a in Leaves (dom d) by A6,XBOOLE_0:def 5; then
A33: not f in Leaves (dom s) by A32,A22,BINTREE1:6,A15,A13; then
A34: f in ( dom s \ (Leaves (dom s)) ) by XBOOLE_0:def 5;
dom s is binary by BINTREE1:def 3;
then A35: succ f = { ( f ^ <* 0 *> ),(f ^ <*1*> ) } by A33;
(f ^ <* 0 *>) in {(f ^ <* 0 *>),(f ^ <*1*>)} by TARSKI:def 2;
then reconsider b1 = (f^<* 0 *> ) as Element of dom s by A35;
(f ^ <* 1 *>) in {(f ^ <* 0 *>),(f ^ <*1*>)} by TARSKI:def 2; then
reconsider c1 = (f^<* 1 *> ) as Element of dom s by A35;
A36: Vtree (f) = Vtree (b1) + Vtree (c1)
by A10,A8,A4,A5,XXREAL_0:2,NAT_1:16,NAT_1:14,A34,A9;
A37: b = <* 1 *> ^b1 by FINSEQ_1:32,A6,A32,A22;
A38: Vtree (b) = Vtree (b1) by A13,A37,Th12;
c = <* 1 *> ^c1 by FINSEQ_1:32,A6,A32,A22;then
Vtree (c) = Vtree (c1) by A13,Th12;
hence Vtree (a) = Vtree (b) + Vtree (c) by A13,A32,A22,Th12,A36,A38;
end;
end;
end;
suppose A39: d = [MaxVl(X) + 1,(Vrootr s) +(Vrootr t)] -tree (s,t);
set bx = [MaxVl(X) + 1,(Vrootr s) +(Vrootr t)];
set q = <*dom s, dom t*>;
A40: len q = 2 by FINSEQ_1:44;
A41: dom (bx -tree (s,t)) = tree ((dom s),(dom t)) by TREES_4:14;
per cases by A41,A39,TREES_3:def 15;
suppose A42: a = {};
A43:Vtree (a) = ( [MaxVl(X) + 1,(Vrootr s) +(Vrootr t)] )`2
by TREES_4:def 4,A39,A42
.= (Vrootr s) +(Vrootr t);
A44: {} in dom s by TREES_1:22;
A45: d.<* 0 *> = d.(<* 0 *>^(<*> NAT) ) by FINSEQ_1:34
.=s.(<*> NAT) by A44,A39,Th11;
A46: Vtree (b) = (Vrootr s) by A45,FINSEQ_1:34,A6,A42;
A47: {} in dom t by TREES_1:22;
d.<* 1 *> = d.(<* 1 *>^(<*> NAT) ) by FINSEQ_1:34
.=t.(<*> NAT) by A47,A39,Th12;
hence Vtree (a) = Vtree (b) + Vtree (c) by A43,A46,FINSEQ_1:34,A6,A42;
end;
suppose ex n being Nat, f being FinSequence st
( n < len q & f in q . (n + 1) & a = <*n*> ^ f ); then
consider n being Nat, f being FinSequence such that
A48: n < len q & f in q . (n + 1) & a = <*n*> ^ f;
per cases by NAT_1:23,A48,A40;
suppose A49:n = 0; then
reconsider f as Element of dom s by A48,FINSEQ_1:44;
A50:Vtree (a) = Vtree (f) by A39,A49,Th11,A48;
not a in Leaves (dom d) by A6,XBOOLE_0:def 5; then
A51: not f in Leaves (dom s) by A49,BINTREE1:6,A41,A39,A48; then
A52: f in ( dom s \ (Leaves (dom s)) ) by XBOOLE_0:def 5;
dom s is binary by BINTREE1:def 3;
then A53:
succ f = { ( f ^ <* 0 *> ),(f ^ <*1*> ) } by A51;
(f ^ <* 0 *>) in {(f ^ <* 0 *>),(f ^ <*1*>)} by TARSKI:def 2;
then reconsider b1 = (f^<* 0 *> ) as Element of dom s by A53;
(f ^ <* 1 *>) in {(f ^ <* 0 *>),(f ^ <*1*>)} by TARSKI:def 2; then
reconsider c1 = (f^<* 1 *> ) as Element of dom s by A53;
A54: Vtree (f) = Vtree (b1) + Vtree (c1)
by A10,A8,A4,A5,XXREAL_0:2,NAT_1:16,NAT_1:14,A52,A9;
A55: b = <* 0 *> ^b1 by FINSEQ_1:32,A6,A49,A48;
A56: Vtree (b) = Vtree (b1) by A39,A55,Th11;
c = <* 0 *> ^c1 by FINSEQ_1:32,A6,A49,A48;
hence Vtree (a) = Vtree (b) + Vtree (c) by A50,A54,A56,A39,Th11;
end;
suppose A57: n = 1; then
reconsider f as Element of dom t by A48,FINSEQ_1:44;
A58:Vtree (a) = Vtree (f) by A39,A57,Th12,A48;
not a in Leaves dom d by A6,XBOOLE_0:def 5; then
A59: not f in Leaves dom t by A57,BINTREE1:6,A41,A39,A48; then
A60: f in ( dom t \ (Leaves dom t)) by XBOOLE_0:def 5;
A61: t in Tseq.i by A10,A9,XBOOLE_0:def 5;
dom t is binary by BINTREE1:def 3; then
A62: succ f = { ( f ^ <* 0 *> ),(f ^ <*1*> ) } by A59;
(f ^ <* 0 *>) in {(f ^ <* 0 *>),(f ^ <*1*>)} by TARSKI:def 2; then
reconsider b1 = (f^<* 0 *> ) as Element of dom t by A62;
(f ^ <* 1 *>) in {(f ^ <* 0 *>),(f ^ <*1*>)} by TARSKI:def 2; then
reconsider c1 = (f^<* 1 *> ) as Element of dom t by A62;
A63: Vtree (f) = Vtree (b1) + Vtree (c1)
by A8,A4,A5,XXREAL_0:2,NAT_1:16,NAT_1:14,A60,A61;
A64: b = <* 1 *> ^b1 by FINSEQ_1:32,A6,A57,A48;
A65: Vtree (b) = Vtree (b1) by A39,A64,Th12;
c = <* 1 *> ^c1 by FINSEQ_1:32,A6,A57,A48;
hence Vtree (a) = Vtree (b) + Vtree (c) by A58,A63,A65,A39,Th12;
end;
end;
end;
end;
end;
end;
A66: for i be Nat holds P[i] from NAT_1:sch 2(A2,A3);
let i be Nat, T be finite binary DecoratedTree of IndexedREAL;
let t,s,r be Element of dom T such that
A67: T in Tseq.i;
i in dom Tseq by A67,FUNCT_1:def 2;
then 1 <= i & i <= len Tseq by FINSEQ_3:25;
hence thesis by A66,A67;
end;
theorem
for t,s,r be 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
A1: ex Tseq,q st Tseq,q,p is_constructingBinHuffmanTree &
{T} = Tseq.(len Tseq) by Def13;
T in {T} by TARSKI:def 1;
hence thesis by A1,Th21;
end;
theorem Th23:
for X be non empty finite Subset of BinFinTrees IndexedREAL st
for T be finite binary DecoratedTree of IndexedREAL st T in X holds
for p be Element of (dom T), r be Element of NAT st r = (T.p) `1
holds r <= MaxVl(X) holds
for s,t,w be finite binary DecoratedTree of IndexedREAL st
s in X & t in X & w= MakeTree (t,s,MaxVl(X) + 1) holds
for p be Element of (dom w), r be Element of NAT st r = (w.p) `1
holds r <= MaxVl(X)+1
proof
let X be non empty finite Subset of BinFinTrees IndexedREAL;
assume A1: for T be finite binary DecoratedTree of IndexedREAL
st T in X holds
for p be Element of (dom T), r be Element of NAT
st r = (T.p) `1
holds r <= MaxVl(X);
let s,t,d be finite binary DecoratedTree of IndexedREAL;
assume
A2:s in X & t in X & d= MakeTree (t,s,MaxVl(X) + 1); then
A3: d.{} = [(MaxVl(X) + 1),(Vrootr t) +(Vrootr s)] by TREES_4:def 4;
set bx = [MaxVl(X) + 1,(Vrootr t) +(Vrootr s)];
set q = <*dom t, dom s*>;
A4: len q = 2 by FINSEQ_1:44;
A5: q.1 = dom t by FINSEQ_1:44;
A6: q.2 = dom s by FINSEQ_1:44;
A7: dom (bx -tree (t,s)) = tree ((dom t),(dom s)) by TREES_4:14;
A8: for a be element st a in dom d holds a = {} or
(ex f be Element of dom t st a = <* 0 *> ^ f ) or
(ex f be Element of dom s st a = <* 1 *> ^ f )
proof
let a be element;
assume A9:a in dom d;
per cases by A9,A2,A7,TREES_3:def 15;
suppose a = {};
hence thesis;
end;
suppose ex n being Nat, f being FinSequence st
( n < len q & f in q . (n + 1) & a = <*n*> ^ f ); then
consider n being Nat, f being FinSequence such that
A10: n < len q & f in q . (n + 1) & a = <*n*> ^ f;
per cases by NAT_1:23,A10,A4;
suppose n = 0;
hence thesis by A10,A5;
end;
suppose n = 1;
hence thesis by A10,A6;
end;
end;
end;
let a be Element of (dom d), r be Element of NAT;
assume A11: r = (d.a) `1;
per cases by A8;
suppose a = {};
hence r <= MaxVl(X)+1 by A11,A3;
end;
suppose ex f be Element of dom t st a = <* 0 *> ^ f;
then
consider f be Element of dom t such that
A12: a = <* 0 *> ^ f;
A13: (d.a) `1 = (t.f) `1 by A12,Th11,A2;
ex x,y be element st x in NAT & y in REAL & t.f = [x,y] by ZFMISC_1:def 2;
then reconsider q= (t.f) `1 as Element of NAT;
q <= MaxVl(X) by A1,A2;
hence r <= MaxVl(X)+1 by A11,A13,NAT_1:16,XXREAL_0:2;
end;
suppose ex f be Element of dom s st a = <* 1 *> ^ f;
then consider f be Element of dom s such that
A14: a = <* 1 *> ^ f;
A15: (d.a) `1 = (s.f) `1 by A14,Th12,A2;
ex x,y be element st x in NAT & y in REAL & s.f = [x,y] by ZFMISC_1:def 2;
then reconsider q= (s.f) `1 as Element of NAT;
q <= MaxVl(X) by A1,A2;
hence r <= MaxVl(X)+1 by A11,A15,NAT_1:16,XXREAL_0:2;
end;
end;
theorem Th24:
Tseq,q,p is_constructingBinHuffmanTree implies
for i be Nat st 1 <=i & i < len Tseq
for X,Y be non empty finite Subset of BinFinTrees IndexedREAL
st X=Tseq.i & Y = Tseq.(i+1) holds
MaxVl(Y)=MaxVl(X) + 1
proof
assume A1:Tseq,q,p is_constructingBinHuffmanTree;
let i be Nat;
assume 1 <=i & i < len Tseq; then
consider X,Y be non empty finite Subset of BinFinTrees IndexedREAL,
s being MinValueTree of X,
t being MinValueTree of Y,
v being finite binary DecoratedTree of IndexedREAL such that
A2: 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} by A1;
let X0,Y0 be non empty finite Subset of BinFinTrees IndexedREAL;
assume A3: X0=Tseq.i & Y0 = Tseq.(i+1);
consider LX0 be non empty finite Subset of NAT such that
A4: LX0 = {Vrootl p where p
is Element of BinFinTrees IndexedREAL: p in X0 }
& MaxVl(X0) = max LX0 by Def9;
consider LY0 be non empty finite Subset of NAT such that
A5: LY0 = {Vrootl p where p
is Element of BinFinTrees IndexedREAL: p in Y0 }
& MaxVl(Y0) = max LY0 by Def9;
v= [(MaxVl(X0) + 1),(Vrootr t) +(Vrootr s)] -tree (t,s) or
v= [(MaxVl(X0) + 1),(Vrootr s) +(Vrootr t)] -tree (s,t)
by TARSKI:def 2, A2,A3; then
A6: v.{} = [(MaxVl(X0) + 1),(Vrootr t) +(Vrootr s)] or
v.{} = [(MaxVl(X0) + 1),(Vrootr s) +(Vrootr t)] by TREES_4:def 4;
dom v is finite & dom v is binary by BINTREE1:def 3; then
reconsider pv=v as Element of BinFinTrees IndexedREAL by Def2;
v in {v} by TARSKI:def 1; then
v in Tseq.(i+1) by A2,XBOOLE_0:def 3; then
A7: Vrootl pv in LY0 by A5,A3;
for x be ExtReal st x in LY0 holds x <= Vrootl pv
proof
let x be ExtReal;
assume x in LY0; then
consider p be Element of BinFinTrees IndexedREAL such that
A8: x=Vrootl p & p in Y0 by A5;
A9: p in (X \ {t,s} ) or p in {v} by XBOOLE_0:def 3,A8,A3,A2;
per cases by A9,TARSKI:def 1,A3,A2,XBOOLE_0:def 5;
suppose p in X0; then
Vrootl p in LX0 by A4; then
Vrootl p <= MaxVl(X0) by A4,XXREAL_2:def 8;
hence x <= Vrootl pv by A6,A8,NAT_1:16,XXREAL_0:2;
end;
suppose p = v;
hence x <= Vrootl pv by A8;
end;
end;
hence MaxVl(Y0) = MaxVl(X0) + 1 by A5,A6,A7,XXREAL_2:def 8;
end;
theorem
Tseq,q,p is_constructingBinHuffmanTree implies
for i be Nat
for X be non empty finite Subset of BinFinTrees IndexedREAL
st X=Tseq.i holds
for T be finite binary DecoratedTree of IndexedREAL st T in X holds
for p be Element of (dom T), r be Element of NAT
st r = (T.p) `1 holds r <= MaxVl(X)
proof
assume A1:Tseq,q,p is_constructingBinHuffmanTree;
defpred P[Nat] means 1 <=$1 & $1 <=len Tseq implies
for X be non empty finite Subset of BinFinTrees IndexedREAL st X=Tseq.$1
holds for T be finite binary DecoratedTree of IndexedREAL st T in X holds
for p be Element of (dom T), r be Element of NAT
st r = (T.p) `1 holds r <= MaxVl(X);
A2: P[0];
A3: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A4: P[i];
assume A5: 1 <=i+1 & i+1 <=len Tseq;
let W be non empty finite Subset of BinFinTrees IndexedREAL;
assume A6: W=Tseq.(i+1);
let d be finite binary DecoratedTree of IndexedREAL;
assume A7: d in W;
per cases;
suppose i = 0; then
consider d0 be Element of FinTrees IndexedREAL such that
A8: d0=d & d0 is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st
d0 = root-tree [ (canFS SOURCE)".x, p.{x} ] by A1,A6,A7;
thus for p be Element of (dom d), r be Element of NAT
st r = (d.p) `1 holds r <= MaxVl(W)
proof
let p be Element of (dom d), r be Element of NAT;
assume A9: r = (d.p) `1;
dom d = {{}} by TREES_1:29,A8,FUNCT_2:def 1; then
A10: r = Vrootl(d) by A9,TARSKI:def 1;
consider L be 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;
end;
end;
suppose A12:i <> 0; then
A13:
1<= i & i < len Tseq by A5,XXREAL_0:2,NAT_1:14,NAT_1:16;
then consider X,Y be 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 be finite binary DecoratedTree of IndexedREAL st T in X holds
for p be Element of (dom T), r be Element of NAT st r = (T.p) `1
holds r <= MaxVl(X) by A4,A12,A5,XXREAL_0:2,NAT_1:14,NAT_1:16,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 be Element of (dom d), r be Element of NAT st r = (d.p) `1
holds r <= MaxVl(W)
proof
let p be Element of (dom d), r be Element of NAT;
assume A20: r = (d.p) `1;
per cases by XBOOLE_0:def 3,A14,A6,A7;
suppose d in (X \ {t,s} );
then d in X by XBOOLE_0:def 5;
then r <= MaxVl(X) by A20,A12,A5,XXREAL_0:2,NAT_1:14,NAT_1:16,A14,A4;
hence r <= MaxVl(W) by A19,XXREAL_0:2,NAT_1:16;
end;
suppose d in {w}; then
d = w by TARSKI:def 1;
hence r <= MaxVl(W) by A17,A19,A16,A20,A18,Th23,A15;
end;
end;
end;
end;
A21: for i be Nat holds P[i] from NAT_1:sch 2(A2,A3);
let i be Nat, X be non empty finite Subset of BinFinTrees IndexedREAL
such that
A22: X=Tseq.i;
let T be finite binary DecoratedTree of IndexedREAL such that
A23: T in X;
i in dom Tseq by A22,FUNCT_1:def 2;
then 1 <= i & i <= len Tseq by FINSEQ_3:25;
hence thesis by A22,A23,A21;
end;
theorem Th26:
Tseq,q,p is_constructingBinHuffmanTree implies
for i be Nat
for X be non empty finite Subset of BinFinTrees IndexedREAL
st X=Tseq.i
for T be finite binary DecoratedTree of IndexedREAL st T in X
for p be Element of (dom T), r be Element of NAT st r = (T.p) `1
holds r <= MaxVl(X)
proof
assume A1:Tseq,q,p is_constructingBinHuffmanTree;
defpred P[Nat] means 1 <=$1 & $1 <=len Tseq implies
for X be non empty finite Subset of BinFinTrees IndexedREAL
st X=Tseq.$1 holds
for T be finite binary DecoratedTree of IndexedREAL
st T in X holds
for p be Element of (dom T), r be Element of NAT
st r = (T.p) `1 holds r <= MaxVl(X);
A2: P[0];
A3: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A4: P[i];
assume A5: 1 <=i+1 & i+1 <=len Tseq;
let W be non empty finite Subset of BinFinTrees IndexedREAL;
assume A6: W=Tseq.(i+1);
let d be finite binary DecoratedTree of IndexedREAL;
assume A7: d in W;
per cases;
suppose i = 0; then
consider d0 be Element of FinTrees IndexedREAL such that
A8: d0=d & d0 is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st
d0 = root-tree [ (canFS SOURCE)".x, p.{x} ] by A1,A6,A7;
thus for p be Element of (dom d), r be Element of NAT
st r = (d.p) `1 holds r <= MaxVl(W)
proof
let p be Element of (dom d), r be Element of NAT;
assume A9: r = (d.p) `1;
dom d = {{}} by TREES_1:29,A8,FUNCT_2:def 1;
then A10: r = Vrootl(d) by A9,TARSKI:def 1;
consider L be 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;
end;
end;
suppose A12:i <> 0; then
A13: 1<= i & i < len Tseq by A5,XXREAL_0:2,NAT_1:16,NAT_1:14;
then consider X,Y be 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 be finite binary DecoratedTree of IndexedREAL st T in X holds
for p be Element of (dom T), r be 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 be Element of (dom d), r be Element of NAT
st r = (d.p) `1 holds r <= MaxVl(W)
proof
let p be Element of (dom d), r be Element of NAT;
assume A20: r = (d.p) `1;
per cases by XBOOLE_0:def 3,A14,A6,A7;
suppose d in (X \ {t,s} );
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;
end;
suppose d in {w};
then d = w by TARSKI:def 1;
hence r <= MaxVl(W) by A17,A19,A16,A20,A18,Th23,A15;
end;
end;
end;
end;
A21: for i be Nat holds P[i] from NAT_1:sch 2(A2,A3);
let i be Nat, X be non empty finite Subset of BinFinTrees IndexedREAL
such that
A22: X=Tseq.i;
let T be finite binary DecoratedTree of IndexedREAL such that
A23: T in X;
i in dom Tseq by A22,FUNCT_1:def 2;
then 1 <= i & i <= len Tseq by FINSEQ_3:25;
hence thesis by A22,A23,A21;
end;
theorem Th27:
Tseq,q,p is_constructingBinHuffmanTree implies
for i be Nat
for s,t be finite binary DecoratedTree of IndexedREAL
for X be non empty finite Subset of BinFinTrees IndexedREAL
st X=Tseq.i & s in X & t in X
for z be finite binary DecoratedTree of IndexedREAL st z in X holds
not [(MaxVl(X) + 1),(Vrootr t) +(Vrootr s)] in rng z
proof
assume A1:Tseq,q,p is_constructingBinHuffmanTree;
let i be Nat;
let s,t be finite binary DecoratedTree of IndexedREAL;
let X be non empty finite Subset of BinFinTrees IndexedREAL;
assume A2: X=Tseq.i & s in X & t in X;
let z be finite binary DecoratedTree of IndexedREAL;
assume A3: z in X;
assume [(MaxVl(X) + 1),(Vrootr t) +(Vrootr s)] in rng z;
then consider p0 be element such that
A4: p0 in dom z
& [(MaxVl(X) + 1),(Vrootr t) +(Vrootr s)] = z.p0 by FUNCT_1:def 3;
reconsider p0 as Element of (dom z) by A4;
ex x,y be element
st x in NAT & y in REAL
& z.p0 = [x,y] by ZFMISC_1:def 2;
then reconsider r = (z.p0) `1 as Element of NAT;
r = MaxVl(X) + 1 by A4;
hence contradiction by NAT_1:16,A3,Th26,A1,A2;
end;
registration
let x be element;
cluster root-tree x -> one-to-one;
coherence
proof
set f = root-tree x;
let x1,x2 be element;
A1: dom root-tree x = elementary_tree 0 by TREES_4:3;
assume x1 in dom f & x2 in dom f & f.x1 = f.x2;
then x1 = {} & x2 = {} by TREES_1:29,TARSKI:def 1,A1;
hence thesis;
end;
end;
theorem Th28:
for X be non empty finite Subset of BinFinTrees IndexedREAL,
s,t,w be finite binary DecoratedTree of IndexedREAL st
( for T be finite binary DecoratedTree of IndexedREAL st T in X holds
for p be Element of (dom T), r be Element of NAT st r = (T.p) `1
holds r <= MaxVl(X) ) &
( for p,q be 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
let X be non empty finite Subset of BinFinTrees IndexedREAL,
s,t,w be finite binary DecoratedTree of IndexedREAL;
assume A1:
( for T be finite binary DecoratedTree of IndexedREAL st T in X holds
for p be Element of (dom T), r be Element of NAT st r = (T.p) `1
holds r <= MaxVl(X) ) &
( for p,q be 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};
set d= MakeTree (t,s,MaxVl(X) + 1);
A2: d.{} = [(MaxVl(X) + 1),(Vrootr t) +(Vrootr s)] by TREES_4:def 4;
set bx = [MaxVl(X) + 1,(Vrootr t) +(Vrootr s)];
set q = <*dom t, dom s*>;
A3: len q = 2 by FINSEQ_1:44;
A4: q.1 = dom t by FINSEQ_1:44;
A5: q.2 = dom s by FINSEQ_1:44;
A6: dom (bx -tree (t,s)) = tree ((dom t),(dom s)) by TREES_4:14;
A7: for a be element st a in dom d holds a = {} or
(ex f be Element of dom t st a = <* 0 *> ^ f ) or
(ex f be Element of dom s st a = <* 1 *> ^ f )
proof
let a be element;
assume A8: a in dom d;
per cases by A8,A6,TREES_3:def 15;
suppose a = {};
hence thesis;
end;
suppose ex n being Nat, f being FinSequence st
( n < len q & f in q . (n + 1) & a = <*n*> ^ f );
then consider n being Nat, f being FinSequence such that
A9: n < len q & f in q . (n + 1) & a = <*n*> ^ f;
per cases by NAT_1:23,A3,A9;
suppose n = 0;
hence thesis by A4,A9;
end;
suppose n = 1;
hence thesis by A9,A5;
end;
end;
end;
assume rng (MakeTree (t,s,(MaxVl(X) + 1)) ) /\ rng w <> {}; then
consider nx be element such that
A10: nx in (rng d ) /\ (rng w ) by XBOOLE_0:def 1;
A11: nx in (rng d ) & nx in (rng w) by XBOOLE_0:def 4,A10;
then consider a0 be element such that
A12: a0 in dom d & nx = d.a0 by FUNCT_1:def 3;
consider b0 be element such that
A13: b0 in dom w & nx = w.b0 by FUNCT_1:def 3,A11;
reconsider a=a0 as Element of (dom d) by A12;
reconsider b=b0 as Element of (dom w) by A13;
A14: w in X & w <> s & w <> t
proof
w in X & not w in {s,t} by A1,XBOOLE_0:def 5;
hence w in X & w <> s & w <> t by TARSKI:def 2;
end; then
A15: rng s /\ rng w = {} by A1;
A16: rng t /\ rng w = {} by A1,A14;
ex x,y be element st x in NAT & y in REAL & w.b = [x,y] by ZFMISC_1:def 2;
then reconsider r = (w.b) `1 as Element of NAT;
per cases by A7;
suppose a = {}; then
(d.a)`1 = MaxVl(X) + 1 by A2;
hence contradiction by NAT_1:16,A1,A14,A12,A13;
end;
suppose ex f be Element of dom t st a = <* 0 *> ^ f; then
consider f be Element of dom t such that
A17: a = <* 0 *> ^ f;
d.a = t.f by A17,Th11; then
d.a in rng t by FUNCT_1:3;
hence contradiction by A16,A12,A11,XBOOLE_0:def 4;
end;
suppose ex f be Element of dom s st a = <* 1 *> ^ f; then
consider f be Element of dom s such that
A18: a = <* 1 *> ^ f;
d.a = s.f by A18,Th12; then
nx in rng s by A12,FUNCT_1:3;
hence contradiction by A15,A11,XBOOLE_0:def 4;
end;
end;
theorem Th29:
Tseq,q,p is_constructingBinHuffmanTree implies
for i be Nat
for T,S be finite binary DecoratedTree of IndexedREAL
st T in Tseq.i & S in Tseq.i & T <> S
holds rng T /\ rng S = {}
proof
assume A1:Tseq,q,p is_constructingBinHuffmanTree;
defpred P[Nat] means 1 <=$1 & $1 <=len Tseq implies
for T,S be finite binary DecoratedTree of IndexedREAL
st T in Tseq.$1 & S in Tseq.$1 & T <> S
holds rng T /\ rng S = {};
A2: P[0];
A3: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A4: P[i];
assume A5: 1 <=i+1 & i+1 <=len Tseq;
let d,h be finite binary DecoratedTree of IndexedREAL;
assume A6: d in Tseq.(i+1) & h in Tseq.(i+1) & d <> h;
per cases;
suppose A7:i = 0; then
consider d0 be Element of FinTrees IndexedREAL such that
A8: d0=d & d0 is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st
d0 = root-tree [ (canFS SOURCE)".x, p.{x} ] by A1,A6;
consider x be Element of SOURCE such that
A9: d0 = root-tree [ (canFS SOURCE)".x, p.{x} ] by A8;
consider h0 be Element of FinTrees IndexedREAL
such that
A10: h0=h & h0 is finite binary DecoratedTree of IndexedREAL &
ex y be Element of SOURCE st
h0 = root-tree [ (canFS SOURCE)".y, p.{y} ] by A7,A1,A6;
consider y be Element of SOURCE such that
A11: h0 = root-tree [ (canFS SOURCE)".y, p.{y} ] by A10;
thus rng d /\ rng h = {}
proof
assume rng d /\ rng h <> {};
then consider z be element
such that A12: z in rng d /\ rng h by XBOOLE_0:def 1;
A13: z in rng d & z in rng h by XBOOLE_0: def 4,A12;
A14: rng d = {[ (canFS SOURCE)".x, p.{x} ]} by A8,A9,FUNCOP_1:8;
A15: rng h = {[ (canFS SOURCE)".y, p.{y} ]} by A10,A11,FUNCOP_1:8;
[ (canFS SOURCE)".x, p.{x} ]
= z by TARSKI:def 1,A14,A13
.= [ (canFS SOURCE)".y, p.{y} ] by TARSKI:def 1,A15,A13;
hence contradiction by A6,A8,A10,A9,A11;
end;
end;
suppose A16:i <> 0; then
1<= i & i < len Tseq by A5,XXREAL_0:2,NAT_1:16,NAT_1:14;
then consider X,Y be 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
A17: 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;
A18: for T be finite binary DecoratedTree of IndexedREAL
st T in X holds
for p be Element of (dom T), r be Element of NAT st r = (T.p) `1
holds r <= MaxVl(X) by A1,A17,Th26;
A19: w = MakeTree (t,s,MaxVl(X) + 1) or
w = MakeTree (s,t,MaxVl(X) + 1) by A17,TARSKI:def 2;
A20: s in X & t in Y by Def10;
then t in X & not t in {s} by A17,XBOOLE_0:def 5;
then
A21: t in X & t <> s by TARSKI:def 1;
per cases by XBOOLE_0:def 3,A17,A6;
suppose d in (X \ {t,s} ) & h in (X \ {t,s} );
then
d in Tseq.i & h in Tseq.i by A17,XBOOLE_0:def 5;
hence rng d /\ rng h = {} by A16,A5,XXREAL_0:2,NAT_1:16,NAT_1:14,A4,A6;
end;
suppose d in {w} & h in (X \ {t,s} );
then
d= w & h in (X \ {t,s} ) by TARSKI:def 1;
hence rng d /\ rng h = {}
by A20,A19,A17,A16,A5,XXREAL_0:2,NAT_1:16,NAT_1:14,A4,A18,A21,Th28;
end;
suppose d in (X \ {t,s} ) & h in {w}; then
d in (X \ {t,s} ) & h = w by TARSKI:def 1;
hence rng d /\ rng h = {} by A20,A19,A16,A5,XXREAL_0:2,NAT_1:16,
NAT_1:14,A4,A18,A17,A21,Th28;
end;
suppose d in {w} & h in {w}; then
d=w & h =w by TARSKI:def 1;
hence rng d /\ rng h = {} by A6;
end;
end;
end;
A22: for i be Nat holds P[i] from NAT_1:sch 2(A2,A3);
let i be Nat, T,S be finite binary DecoratedTree of IndexedREAL such that
A23: T in Tseq.i & S in Tseq.i & T <> S;
i in dom Tseq by A23,FUNCT_1:def 2;
then 1 <= i & i <= len Tseq by FINSEQ_3:25;
hence thesis by A23,A22;
end;
theorem Th30:
for X be non empty finite Subset of BinFinTrees IndexedREAL,
s,t be 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 be 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
let X be non empty finite Subset of BinFinTrees
IndexedREAL,
s,t be finite binary DecoratedTree of IndexedREAL;
assume
A1: s is one-to-one & t is one-to-one & t in X & s in X
& rng s /\ rng t = {}
& ( for z be finite binary DecoratedTree of IndexedREAL st z in X holds
not [(MaxVl(X) + 1),(Vrootr t) +(Vrootr s)] in rng z );
set d = MakeTree (t,s,(MaxVl(X) + 1));
A2: d.{} = [(MaxVl(X) + 1),(Vrootr t) +(Vrootr s)] by TREES_4:def 4;
set bx = [MaxVl(X) + 1,(Vrootr t) +(Vrootr s)];
set q = <*dom t, dom s*>;
A3: len q = 2 by FINSEQ_1:44;
A4: q.1 = dom t by FINSEQ_1:44;
A5: q.2 = dom s by FINSEQ_1:44;
A6: dom (bx -tree (t,s)) = tree ((dom t),(dom s)) by TREES_4:14;
A7: for a be element st a in dom d holds a = {} or
(ex f be Element of dom t st a = <* 0 *> ^ f ) or
(ex f be Element of dom s st a = <* 1 *> ^ f )
proof
let a be element;
assume A8: a in dom d;
per cases by A6,TREES_3:def 15,A8;
suppose a = {};
hence thesis;
end;
suppose ex n being Nat, f being FinSequence st
( n < len q & f in q . (n + 1) & a = <*n*> ^ f ); then
consider n being Nat, f being FinSequence such that
A9: n < len q & f in q . (n + 1) & a = <*n*> ^ f;
per cases by NAT_1:23,A3,A9;
suppose n = 0;
hence thesis by A4,A9;
end;
suppose n = 1;
hence thesis by A9,A5;
end;
end;
end;
A10: for x be element st x in dom d & x <> {} holds d.x <> d.{}
proof
let x be element;
assume A11: x in dom d & x <> {};
per cases by A11,A7;
suppose ex f be Element of dom t st x = <* 0 *> ^ f;
then consider f be Element of dom t such that
A12: x = <* 0 *> ^ f;
d.x = t.f by A12,Th11;
hence d.x <> d.{} by FUNCT_1:3,A1,A2;
end;
suppose ex f be Element of dom s st x = <* 1 *> ^ f;
then consider f be Element of dom s such that
A13: x = <* 1 *> ^ f;
d.x = s.f by A13,Th12;
hence d.x <> d.{} by FUNCT_1:3,A1,A2;
end;
end;
A14: for x1,x2 be element
st x1 in dom d & x2 in dom d & d.x1 = d.x2 holds
not ((ex f be Element of dom s st x1 = <* 1 *> ^ f ) &
(ex f be Element of dom t st x2 = <* 0 *> ^ f ))
proof
let x1,x2 be element;
assume A15: x1 in dom d & x2 in dom d & d.x1 = d.x2;
assume A16: (ex f be Element of dom s st x1 = <* 1 *> ^ f ) &
(ex f be Element of dom t st x2 = <* 0 *> ^ f );
then consider f be Element of dom s such that
A17: x1 = <* 1 *> ^ f;
A18: d.x1 = s.f by A17,Th12;
consider g be Element of dom t such that
A19: x2 = <* 0 *> ^ g by A16;
A20: s.f = t.g by A15,A18,A19,Th11;
s.f in rng s & t.g in rng t by FUNCT_1:3;
hence contradiction by A1,XBOOLE_0:def 4,A20;
end;
for x1,x2 be element st x1 in dom d & x2 in dom d
& d.x1 = d.x2 holds x1 = x2
proof
let x1,x2 be element;
assume A21: x1 in dom d & x2 in dom d & d.x1 = d.x2;
per cases;
suppose x1 = {} & x2 = {};
hence thesis;
end;
suppose x1 = {} & x2 <> {};
hence thesis by A21,A10;
end;
suppose x1 <> {} & x2 = {};
hence thesis by A21,A10;
end;
suppose
A22: x1 <> {} & x2 <> {}; then
A23: (ex f be Element of dom t st x1 = <* 0 *> ^ f ) or
(ex f be Element of dom s st x1 = <* 1 *> ^ f ) by A21,A7;
A24: (ex f be Element of dom t st x2 = <* 0 *> ^ f ) or
(ex f be Element of dom s st x2 = <* 1 *> ^ f ) by A21,A7,A22;
per cases by A23,A24,A21,A14;
suppose A25:
( (ex f be Element of dom t st x1 = <* 0 *> ^ f ) &
(ex f be Element of dom t st x2 = <* 0 *> ^ f ) );
then consider f be Element of dom t such that
A26: x1 = <* 0 *> ^ f;
A27: d.x1 = t.f by A26,Th11;
consider g be Element of dom t such that
A28: x2 = <* 0 *> ^ g by A25;
d.x2 = t.g by A28,Th11;
hence x1=x2 by A26,A28,A1,FUNCT_1:def 4,A21,A27;
end;
suppose A29:
( (ex f be Element of dom s st x1 = <* 1 *> ^ f ) &
(ex f be Element of dom s st x2 = <* 1 *> ^ f ) ); then
consider f be Element of dom s such that
A30: x1 = <* 1 *> ^ f;
A31: d.x1 = s.f by A30,Th12;
consider g be Element of dom s such that
A32: x2 = <* 1 *> ^ g by A29;
d.x2 = s.g by A32,Th12;
hence x1=x2 by A30,A32,A1,FUNCT_1:def 4,A21,A31;
end;
end;
end;
hence thesis by FUNCT_1:def 4;
end;
theorem Th31:
Tseq,q,p is_constructingBinHuffmanTree implies
for i be Nat
for T be finite binary DecoratedTree of IndexedREAL
st T in Tseq.i
holds T is one-to-one
proof
assume A1:Tseq,q,p is_constructingBinHuffmanTree;
defpred P[Nat] means 1 <=$1 & $1 <=len Tseq implies
for T be finite binary DecoratedTree of IndexedREAL st T in Tseq.$1
holds T is one-to-one;
A2: P[0];
A3: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A4: P[i];
assume A5: 1 <=i+1 & i+1 <=len Tseq;
let d be finite binary DecoratedTree of IndexedREAL;
assume A6: d in Tseq.(i+1);
per cases;
suppose i = 0;
then
ex d0 be Element of FinTrees IndexedREAL st
d0=d & d0 is finite binary DecoratedTree of IndexedREAL &
ex x be Element of SOURCE st
d0 = root-tree [ (canFS SOURCE)".x, p.{x} ] by A1,A6;
hence d is one-to-one;
end;
suppose A7:i <> 0;
then 1<= i & i < len Tseq by A5,XXREAL_0:2,NAT_1:16,NAT_1:14;
then consider X,Y be 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
A8: 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;
A9: w = MakeTree (t,s,MaxVl(X) + 1) or
w = MakeTree (s,t,MaxVl(X) + 1) by A8,TARSKI:def 2;
A10: s in X & t in Y by Def10; then
A11:t in X & not t in {s} by A8,XBOOLE_0:def 5;
then
A12: t in X & t <> s by TARSKI:def 1;
A13: for z be finite binary DecoratedTree of IndexedREAL st z in X holds
not [(MaxVl(X) + 1),(Vrootr t) +(Vrootr s)] in rng z
by A10,A1,Th27,A8,A11;
A14: s is one-to-one & t is one-to-one by A10,A11,A8,A4,
A5,XXREAL_0:2,NAT_1:16,NAT_1:14,A7;
A15: rng s /\ rng t = {} by A10,A12,A8,Th29,A1;
per cases by XBOOLE_0:def 3,A8,A6;
suppose d in (X \ {t,s} ); then
d in X & not d in {t,s} by XBOOLE_0:def 5;
hence d is one-to-one by A7,A5,XXREAL_0:2,NAT_1:16,NAT_1:14,A4,A8;
end;
suppose A16: d in {w};
per cases by A16,TARSKI:def 1,A9;
suppose d =MakeTree (t,s,MaxVl(X) + 1);
hence d is one-to-one by A10,Th30,A13,A11,A14,A15;
end;
suppose d =MakeTree (s,t,MaxVl(X) + 1);
hence d is one-to-one by A10,Th30,A13,A11,A14,A15;
end;
end;
end;
end;
A17: for i be Nat holds P[i] from NAT_1:sch 2(A2,A3);
let i be Nat;
let T be finite binary DecoratedTree of IndexedREAL such that
A18: T in Tseq.i;
i in dom Tseq by A18,FUNCT_1:def 2;
then 1 <= i & i <= len Tseq by FINSEQ_3:25;
hence thesis by A18,A17;
end;
registration
let SOURCE,p;
::$MR Now we are at the position where we can present the Main Theorem of the paper
cluster -> one-to-one for BinHuffmanTree of p;
coherence
proof
let T be BinHuffmanTree of p;
A1: ex Tseq,q st Tseq,q,p is_constructingBinHuffmanTree & {T} = Tseq.(len Tseq)
by Def13;
T in {T} by TARSKI:def 1;
hence thesis by A1,Th31;
end;
end;