HUFFMAN1

:: Constructing Binary {H}uffman Tree
::  by Hiroyuki Okazaki , Yuichi Futa and Yasunari Shidama
::
:: Received June 18, 2013
:: Copyright (c) 2013-2026 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,
      ORDINAL1,
      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, NUMBERS, FRAENKEL, XXREAL_2,
      FUNCOP_1;
 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;
  coherence;
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[object] 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 object 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 object;
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 object;
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 object;
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 object;
 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 object 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 object;
 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 object 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;
 then T is Element of FinTrees IndexedREAL by A3,TREES_3:def 8; then
A4: T in S;
for z be object st z in S holds z in
Funcs(elementary_tree 0,[:Seg (card SOURCE),rng p:])
proof
 let z be object;
 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;
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 object 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 object 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 object 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 object;
 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 by TARSKI:1;
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 object st n in L holds n = Vrootl w
proof
let n be object;
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 object st n = Vrootl w holds n in L
proof
let n be object;
assume A4: n = Vrootl w;
consider y be object 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 object 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 object 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 object
 st ex u,v be object st u <> v & u in X & v in X holds
 X \ {x} <> {}
proof
let X be set,x be object;
 assume A1:
 ex u,v be object st u <> v & u in X & v in X;
 assume
 A2: not X \ {x} <> {};
A3: now let z be object;
 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 object 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 object
 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 object;
 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 object 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 object st u <> v & u in X & v in X;
 X <> {} by A1; then
 consider z be object such that A3: z in X by XBOOLE_0:def 1;
 A4: {z} c= X by ZFMISC_1:31,A3;
 now let x be object;
 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 object 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 object st X = {u} by CARD_1:29;
end;

Lm5:
 for X be finite set, t,s,z be object
 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 object;
 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[object,object] means $2= root-tree [ fcs.$1, p.{$1} ];
A1: for x being object st x in SOURCE
 ex y being object st y in Initial-Trees(p) & P[x,y]
proof
 let x be object;
 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;
 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 object st x in SOURCE holds P[x,f.x]
from FUNCT_2:sch 1(A1);
now let x1,x2 be object;
 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 object;
 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 object;
 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 object holds x in LeavesSet({X}) iff x in {Leaves X}
 proof
 let x be object;
 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 object
 holds x in LeavesSet(X \/ Y) iff x in LeavesSet(X) \/ LeavesSet(Y)
 proof
 let x be object;
 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*>;
 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 object holds p in tree (t,s) iff p in elementary_tree 0
 proof
 let p0 be object;
 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;
 for x be object holds x in H iff x in L \/ R
 proof
 let x be object;
 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,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;
 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); 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; 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 object,
 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 object, 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;
 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 object,
 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 object,
 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;
 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 object holds
 Leaves (x-tree (t,s)) = (Leaves t) \/ Leaves s
proof
 let s,t be DecoratedTree, x be object;
 set q = <*dom t,dom s*>;
 A1: len q = 2 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 object holds
 z in ((x-tree(t,s)) .: L) iff z in t .: (Leaves dom t)
proof
let z be object;
 hereby assume z in ((x-tree(t,s)) .: L);
 then consider q be object 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 object 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); 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 object holds
 z in ((x-tree(t,s)) .: R) iff z in s .: (Leaves (dom s ))
proof
let z be object;
 hereby assume z in ((x-tree(t,s)) .: R);
 then consider q be object 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 object 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; 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 object holds
 x in Leaves (elementary_tree 0 ) iff x in elementary_tree 0
proof
 let x be object;
 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 object, 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 object, 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 A1;
 A5: Leaves dom T = {{}} by TREES_1:29,Th15,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 object 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 object st u <> v & u in x & v in x;
 then consider u,v be object 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[object,object] 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 object 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 object 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 object such that
 A41: Tseqk = {u} by Lm4,A12,A38,A40;
 card SOURCE in dom Tseq by FINSEQ_1:def 3,A5,A39; then
A42: Tseq.(card SOURCE) in rng Tseq by FUNCT_1:3;
A43: u in Tseqk by TARSKI:def 1,A41;
 then reconsider T = u as DecoratedTree of IndexedREAL by A40,A42;
 A44: dom T is finite & T is binary by A43, Def2,A40,A42;
 reconsider T 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 object holds x in L iff x in R
proof
 let x be object;
 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;
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;
 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;
 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;
 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;
 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;
 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;
 A7: dom (bx -tree (t,s)) = tree ((dom t),(dom s)) by TREES_4:14;
A8: for a be object 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 object;
 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;
 end;
 suppose n = 1;
   hence thesis by A10;
 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 object 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 object 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; 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;
 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 object 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 object
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 object;
 cluster root-tree x -> one-to-one;
 coherence
proof
 set f = root-tree x;
 let x1,x2 be object;
 assume x1 in dom f & x2 in dom f & f.x1 = f.x2;
 then x1 = {} & x2 = {} by TREES_1:29,TARSKI:def 1;
 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;
 A6: dom (bx -tree (t,s)) = tree ((dom t),(dom s)) by TREES_4:14;
A7: for a be object 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 object;
 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 A9;
 end;
 suppose n = 1;
   hence thesis by A9;
 end;
 end;
end;
assume rng (MakeTree (t,s,(MaxVl(X) + 1)) ) /\ rng w <> {}; then
 consider nx be object 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 object such that
 A12: a0 in dom d & nx = d.a0 by FUNCT_1:def 3;
 consider b0 be object 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 object 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 object
 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;
 A6: dom (bx -tree (t,s)) = tree ((dom t),(dom s)) by TREES_4:14;
A7: for a be object 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 object;
 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 A9;
 end;
 suppose n = 1;
   hence thesis by A9;
 end;
 end;
end;

A10: for x be object st x in dom d & x <> {} holds d.x <> d.{}
proof
 let x be object;
 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 object
 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 object;
 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 object st x1 in dom d & x2 in dom d
 & d.x1 = d.x2 holds x1 = x2
proof
 let x1,x2 be object;
 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;
  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;