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
for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)
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
for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)
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
for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)
let q be FinSequence of NAT ; ( Tseq,q,p is_constructingBinHuffmanTree implies for i being Nat
for T being finite binary DecoratedTree of IndexedREAL
for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r) )
assume A1:
Tseq,q,p is_constructingBinHuffmanTree
; for i being Nat
for T being finite binary DecoratedTree of IndexedREAL
for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)
defpred S2[ Nat] means ( 1 <= $1 & $1 <= len Tseq implies for T being finite binary DecoratedTree of IndexedREAL
for a, b, c being 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:
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
for a, b, c being Element of dom T st T in Tseq . (i + 1) & a in (dom T) \ (Leaves (dom T)) & b = a ^ <*0*> & c = a ^ <*1*> holds
Vtree a = (Vtree b) + (Vtree c)
let d be
finite binary DecoratedTree of
IndexedREAL ;
for a, b, c being Element of dom d st d in Tseq . (i + 1) & a in (dom d) \ (Leaves (dom d)) & b = a ^ <*0*> & c = a ^ <*1*> holds
Vtree a = (Vtree b) + (Vtree c)let a,
b,
c be
Element of
dom d;
( d in Tseq . (i + 1) & a in (dom d) \ (Leaves (dom d)) & b = a ^ <*0*> & c = a ^ <*1*> implies Vtree a = (Vtree b) + (Vtree c) )
assume A6:
(
d in Tseq . (i + 1) &
a in (dom d) \ (Leaves (dom d)) &
b = a ^ <*0*> &
c = a ^ <*1*> )
;
Vtree a = (Vtree b) + (Vtree c)
per cases
( i = 0 or i <> 0 )
;
suppose A8:
i <> 0
;
Vtree a = (Vtree b) + (Vtree c)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 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
( d in X \ {t,s} or d in {w} )
by XBOOLE_0:def 3, A9, A6;
suppose A12:
d in {w}
;
Vtree a = (Vtree b) + (Vtree c)per cases
( d = [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] -tree (t,s) or d = [((MaxVl X) + 1),((Vrootr s) + (Vrootr t))] -tree (s,t) )
by A12, TARSKI:def 1, A11;
suppose A13:
d = [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] -tree (
t,
s)
;
Vtree a = (Vtree b) + (Vtree c)set bx =
[((MaxVl X) + 1),((Vrootr t) + (Vrootr s))];
set q =
<*(dom t),(dom s)*>;
A14:
len <*(dom t),(dom s)*> = 2
by FINSEQ_1:44;
A15:
dom ([((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] -tree (t,s)) = tree (
(dom t),
(dom s))
by TREES_4:14;
per cases
( a = {} or ex n being Nat ex f being FinSequence st
( n < len <*(dom t),(dom s)*> & f in <*(dom t),(dom s)*> . (n + 1) & a = <*n*> ^ f ) )
by A15, A13, TREES_3:def 15;
suppose A16:
a = {}
;
Vtree a = (Vtree b) + (Vtree c)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;
verum end; suppose
ex
n being
Nat ex
f being
FinSequence st
(
n < len <*(dom t),(dom s)*> &
f in <*(dom t),(dom s)*> . (n + 1) &
a = <*n*> ^ f )
;
Vtree a = (Vtree b) + (Vtree c)then consider n being
Nat,
f being
FinSequence such that A22:
(
n < len <*(dom t),(dom s)*> &
f in <*(dom t),(dom s)*> . (n + 1) &
a = <*n*> ^ f )
;
per cases
( n = 0 or n = 1 )
by NAT_1:23, A22, A14;
suppose A23:
n = 0
;
Vtree a = (Vtree b) + (Vtree c)then reconsider f =
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;
verum end; suppose A32:
n = 1
;
Vtree a = (Vtree b) + (Vtree c)then reconsider f =
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;
verum end; end; end; end; end; suppose A39:
d = [((MaxVl X) + 1),((Vrootr s) + (Vrootr t))] -tree (
s,
t)
;
Vtree a = (Vtree b) + (Vtree c)set bx =
[((MaxVl X) + 1),((Vrootr s) + (Vrootr t))];
set q =
<*(dom s),(dom t)*>;
A40:
len <*(dom s),(dom t)*> = 2
by FINSEQ_1:44;
A41:
dom ([((MaxVl X) + 1),((Vrootr s) + (Vrootr t))] -tree (s,t)) = tree (
(dom s),
(dom t))
by TREES_4:14;
per cases
( a = {} or ex n being Nat ex f being FinSequence st
( n < len <*(dom s),(dom t)*> & f in <*(dom s),(dom t)*> . (n + 1) & a = <*n*> ^ f ) )
by A41, A39, TREES_3:def 15;
suppose A42:
a = {}
;
Vtree a = (Vtree b) + (Vtree c)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;
verum end; suppose
ex
n being
Nat ex
f being
FinSequence st
(
n < len <*(dom s),(dom t)*> &
f in <*(dom s),(dom t)*> . (n + 1) &
a = <*n*> ^ f )
;
Vtree a = (Vtree b) + (Vtree c)then consider n being
Nat,
f being
FinSequence such that A48:
(
n < len <*(dom s),(dom t)*> &
f in <*(dom s),(dom t)*> . (n + 1) &
a = <*n*> ^ f )
;
per cases
( n = 0 or n = 1 )
by NAT_1:23, A48, A40;
suppose A49:
n = 0
;
Vtree a = (Vtree b) + (Vtree c)then reconsider f =
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;
verum end; suppose A57:
n = 1
;
Vtree a = (Vtree b) + (Vtree c)then reconsider f =
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;
verum end; end; end; end; end; end; end; end; end; end;
end;
A66:
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
for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)
let T be finite binary DecoratedTree of IndexedREAL ; for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)
let t, s, r be Element of dom T; ( T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> implies Vtree t = (Vtree s) + (Vtree r) )
assume A67:
T in Tseq . i
; ( not t in (dom T) \ (Leaves (dom T)) or not s = t ^ <*0*> or not r = t ^ <*1*> or Vtree t = (Vtree s) + (Vtree r) )
i in dom Tseq
by A67, FUNCT_1:def 2;
then
( 1 <= i & i <= len Tseq )
by FINSEQ_3:25;
hence
( not t in (dom T) \ (Leaves (dom T)) or not s = t ^ <*0*> or not r = t ^ <*1*> or Vtree t = (Vtree s) + (Vtree r) )
by A66, A67; verum