huffman1.miz



    begin

    registration

      let D be non empty set, x be Element of D;

      cluster ( root-tree x) -> binary;

      coherence ;

    end

    definition

      :: HUFFMAN1:def1

      func IndexedREAL -> set equals [: NAT , REAL :];

      correctness ;

    end

    registration

      cluster IndexedREAL -> non empty;

      coherence ;

    end

    definition

      let D be non empty set;

      :: HUFFMAN1:def2

      func BinFinTrees D -> DTree-set of D means

      : Def2: for T be DecoratedTree of D holds ( dom T) is finite & T is binary iff T in it ;

      existence

      proof

        defpred S1[ object] means ex T be DecoratedTree of D st $1 = T & ( dom T) is finite & T is binary;

        consider X be set such that

         A1: for x be 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 be 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 be DecoratedTree of D holds (( dom T) is finite & T is binary) iff T in T1 and

         A4: for T be 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;

      :: HUFFMAN1:def3

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

      correctness

      proof

        set L = { x where x be 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;

      :: HUFFMAN1:def4

      func Initial-Trees (p) -> non empty finite Subset of ( BinFinTrees IndexedREAL ) equals { T where T be 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 be 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;

      :: HUFFMAN1:def5

      func Vrootr p -> Real equals ((p . {} ) `2 );

      correctness by A1;

      :: HUFFMAN1:def6

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

      :: HUFFMAN1:def7

      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;

      :: HUFFMAN1:def8

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

      :: HUFFMAN1:def9

      func MaxVl (X) -> Nat means

      : Def9: ex L be non empty finite Subset of NAT st L = { ( Vrootl p) where p be Element of ( BinFinTrees IndexedREAL ) : p in X } & it = ( max L);

      existence

      proof

        set L = { ( Vrootl p) where p be 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 :: HUFFMAN1:1

    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 be 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 :: HUFFMAN1:2

    

     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 be 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 be 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 be 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 :: HUFFMAN1:3

    for X,Z be non empty finite Subset of ( BinFinTrees IndexedREAL ) holds 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 :: HUFFMAN1:4

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

      :: HUFFMAN1:def10

      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 holds 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 :: HUFFMAN1:5

    

     Th5: ( card ( Initial-Trees p)) = ( card SOURCE)

    proof

      set L = { T where T be 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 be object st x in SOURCE holds ex y be 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 be Function of SOURCE, ( Initial-Trees p) such that

       A5: for x be 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 :: HUFFMAN1:6

    

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

      :: HUFFMAN1:def11

      func LeavesSet (X) -> Subset of ( bool IndexedREAL ) equals { ( Leaves p) where p be Element of ( BinFinTrees IndexedREAL ) : p in X };

      correctness

      proof

        set L = { ( Leaves p) where p be 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 :: HUFFMAN1:7

    

     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 :: HUFFMAN1:8

    

     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 :: HUFFMAN1:9

    

     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 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 be FinSequence of NAT , n be 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 :: HUFFMAN1:10

    

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

    proof

      let s,t be Tree;

      set L = { ( <* 0 *> ^ p) where p be Element of t : p in ( Leaves t) };

      set R = { ( <*1*> ^ p) where p be 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 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 be Nat, r be FinSequence st (n < ( len q) & r in (q . (n + 1)) & x = ( <*n*> ^ r)) by TREES_3:def 15;

          then

          consider n be Nat, r be 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 :: HUFFMAN1:11

    

     Th11: for s,t be DecoratedTree, x be object, q be 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 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 :: HUFFMAN1:12

    

     Th12: for s,t be DecoratedTree, x be object, q be 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 be 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 :: HUFFMAN1:13

    

     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;

      

       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 be Element of ( dom t) : p in ( Leaves ( dom t)) } \/ { ( <*1*> ^ p) where p be Element of ( dom s) : p in ( Leaves ( dom s)) }) by Th10;

      set L = { ( <* 0 *> ^ p) where p be Element of ( dom t) : p in ( Leaves ( dom t)) };

      set R = { ( <*1*> ^ p) where p be 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 be 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)) 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 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 be 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, 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 :: HUFFMAN1:14

    

     Th14: for k be Nat holds 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 :: HUFFMAN1:15

    

     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 :: HUFFMAN1:16

    

     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

    definition

      let SOURCE, p, Tseq, q;

      :: HUFFMAN1:def12

      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) holds ex X,Y be non empty finite Subset of ( BinFinTrees IndexedREAL ), s be MinValueTree of X, t be MinValueTree of Y, v be 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 :: HUFFMAN1:17

    

     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 be non empty finite Subset of ( BinFinTrees IndexedREAL ), s be MinValueTree of X, t be MinValueTree of Y, w be 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 be Nat st 1 <= n & n < ( card SOURCE) holds for x be Element of ( BoolBinFinTrees IndexedREAL ) holds ex y be 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 be Element of ( BoolBinFinTrees IndexedREAL ) st ex X,Y be non empty finite Subset of ( BinFinTrees IndexedREAL ), s be MinValueTree of X, t be MinValueTree of Y, w be 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 be FinSequence of ( BoolBinFinTrees IndexedREAL ) such that

       A5: ( len Tseq) = ( card SOURCE) & ((Tseq . 1) = ITS or ( card SOURCE) = 0 ) & (for n be 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)) holds ex x be 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 be 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 be MinValueTree of X, t be MinValueTree of Y, w be 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 be MinValueTree of X, t be MinValueTree of Y, w be 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 be MinValueTree of X, t be MinValueTree of Y, w be 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 be MinValueTree of X, t be MinValueTree of Y, w be 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, NAT_1: 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;

      :: HUFFMAN1:def13

      mode BinHuffmanTree of p -> finite binary DecoratedTree of IndexedREAL means

      : Def13: ex Tseq be FinSequence of ( BoolBinFinTrees IndexedREAL ), q be 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 :: HUFFMAN1:18

    

     Th18: ( union ( LeavesSet ( Initial-Trees p))) = { z where z be 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 be 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 :: HUFFMAN1:19

    

     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 be 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 be 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 be MinValueTree of X, t be MinValueTree of Y, w be 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 be 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 be Element of [: NAT , REAL :] : ex x be Element of SOURCE st z = [((( canFS SOURCE) " ) . x), (p . {x})] } by A13;

      hence thesis;

    end;

    theorem :: HUFFMAN1:20

    ( Leaves T) = { z where z be 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 be 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 be 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 :: HUFFMAN1:21

    

     Th21: (Tseq,q,p) is_constructingBinHuffmanTree implies for i be Nat holds for T be finite binary DecoratedTree of IndexedREAL holds 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 holds 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 be MinValueTree of X, t be MinValueTree of Y, w be 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 be Nat, f be FinSequence st (n < ( len q) & f in (q . (n + 1)) & a = ( <*n*> ^ f));

                then

                consider n be Nat, f be 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 be Nat, f be FinSequence st (n < ( len q) & f in (q . (n + 1)) & a = ( <*n*> ^ f));

                then

                consider n be Nat, f be 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 :: HUFFMAN1:22

    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 :: HUFFMAN1:23

    

     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 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 be Nat, f be FinSequence st (n < ( len q) & f in (q . (n + 1)) & a = ( <*n*> ^ f));

          then

          consider n be Nat, f be 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 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 :: HUFFMAN1:24

    

     Th24: (Tseq,q,p) is_constructingBinHuffmanTree implies for i be Nat st 1 <= i & i < ( len Tseq) holds 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 be MinValueTree of X, t be MinValueTree of Y, v be 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 be 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 be 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 :: HUFFMAN1:25

    (Tseq,q,p) is_constructingBinHuffmanTree implies for i be Nat holds 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 be 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 be MinValueTree of X, t be MinValueTree of Y, w be 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 :: HUFFMAN1:26

    

     Th26: (Tseq,q,p) is_constructingBinHuffmanTree implies for i be Nat holds 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 be 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 be MinValueTree of X, t be MinValueTree of Y, w be 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 :: HUFFMAN1:27

    

     Th27: (Tseq,q,p) is_constructingBinHuffmanTree implies for i be Nat holds for s,t be finite binary DecoratedTree of IndexedREAL holds for X be non empty finite Subset of ( BinFinTrees IndexedREAL ) st X = (Tseq . i) & s in X & t in X holds 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 :: HUFFMAN1:28

    

     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 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 be Nat, f be FinSequence st (n < ( len q) & f in (q . (n + 1)) & a = ( <*n*> ^ f));

          then

          consider n be Nat, f be 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 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 :: HUFFMAN1:29

    

     Th29: (Tseq,q,p) is_constructingBinHuffmanTree implies for i be Nat holds 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 be MinValueTree of X, t be MinValueTree of Y, w be 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 :: HUFFMAN1:30

    

     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 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 be Nat, f be FinSequence st (n < ( len q) & f in (q . (n + 1)) & a = ( <*n*> ^ f));

          then

          consider n be Nat, f be 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 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 :: HUFFMAN1:31

    

     Th31: (Tseq,q,p) is_constructingBinHuffmanTree implies for i be Nat holds 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 be MinValueTree of X, t be MinValueTree of Y, w be 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