let SOURCE be non empty finite set ; for p being Probability of Trivial-SigmaField SOURCE
for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one
let p be Probability of Trivial-SigmaField SOURCE; for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one
let Tseq be FinSequence of BoolBinFinTrees IndexedREAL; for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one
let q be FinSequence of NAT ; ( Tseq,q,p is_constructingBinHuffmanTree implies for i being Nat
for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one )
assume A1:
Tseq,q,p is_constructingBinHuffmanTree
; for i being Nat
for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one
defpred S2[ Nat] means ( 1 <= $1 & $1 <= len Tseq implies for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . $1 holds
T is one-to-one );
A2:
S2[ 0 ]
;
A3:
for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be
Nat;
( S2[i] implies S2[i + 1] )
assume A4:
S2[
i]
;
S2[i + 1]
assume A5:
( 1
<= i + 1 &
i + 1
<= len Tseq )
;
for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . (i + 1) holds
T is one-to-one
let d be
finite binary DecoratedTree of
IndexedREAL ;
( d in Tseq . (i + 1) implies d is one-to-one )
assume A6:
d in Tseq . (i + 1)
;
d is one-to-one
per cases
( i = 0 or i <> 0 )
;
suppose A7:
i <> 0
;
d is one-to-one then
( 1
<= i &
i < len Tseq )
by A5, XXREAL_0:2, NAT_1:16, NAT_1:14;
then consider X,
Y being non
empty finite Subset of
(BinFinTrees IndexedREAL),
s being
MinValueTree of
X,
t being
MinValueTree of
Y,
w being
finite binary DecoratedTree of
IndexedREAL such that 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 being
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;
end;
end;
A17:
for i being Nat holds S2[i]
from NAT_1:sch 2(A2, A3);
let i be Nat; for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one
let T be finite binary DecoratedTree of IndexedREAL ; ( T in Tseq . i implies T is one-to-one )
assume A18:
T in Tseq . i
; T is one-to-one
i in dom Tseq
by A18, FUNCT_1:def 2;
then
( 1 <= i & i <= len Tseq )
by FINSEQ_3:25;
hence
T is one-to-one
by A18, A17; verum