let SOURCE be non empty finite set ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( S2[i] implies S2[i + 1] )
assume A4: S2[i] ; :: thesis: S2[i + 1]
assume A5: ( 1 <= i + 1 & i + 1 <= len Tseq ) ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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*> ) ; :: thesis: Vtree a = (Vtree b) + (Vtree c)
per cases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; :: thesis: Vtree a = (Vtree b) + (Vtree c)
then consider d0 being Element of FinTrees IndexedREAL such that
A7: ( d0 = d & d0 is finite binary DecoratedTree of IndexedREAL & ex x being 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; :: thesis: verum
end;
suppose A8: i <> 0 ; :: thesis: 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} ; :: thesis: 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) ; :: thesis: 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 = {} ; :: thesis: 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; :: thesis: 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 ) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose A32: n = 1 ; :: thesis: 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; :: thesis: verum
end;
end;
end;
end;
end;
suppose A39: d = [((MaxVl X) + 1),((Vrootr s) + (Vrootr t))] -tree (s,t) ; :: thesis: 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 = {} ; :: thesis: 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; :: thesis: 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 ) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose A57: n = 1 ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum