let SOURCE be non empty finite set ; :: thesis:
let p be Probability of Trivial-SigmaField SOURCE; :: thesis:
let Tseq be FinSequence of BoolBinFinTrees IndexedREAL; :: thesis:
let q be FinSequence of NAT ; :: thesis:
assume A1: Tseq,q,p is_constructingBinHuffmanTree ; :: thesis:
defpred S₂[ 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: S₂[ 0 ] ;
A3: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis:
assume A4: S₂[i] ; :: thesis:
assume A5: ( 1 <= i + 1 & i + 1 <= len Tseq ) ; :: thesis:
let d be finite binary DecoratedTree of IndexedREAL ; :: thesis:
let a, b, c be Element of dom d; :: thesis:
assume A6: ( d in Tseq . (i + 1) & a in (dom d) \ (Leaves (dom d)) & b = a ^ <*0*> & c = a ^ <*1*> ) ; :: thesis:

per cases ;

suppose i = 0 ; :: thesis:

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:

end;

suppose A8: i <> 0 ; :: thesis:

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 by XBOOLE_0:def 3, A9, A6;

suppose d in X \ {t,s} ; :: thesis:

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; :: thesis:

end;

suppose A12: d in {w} ; :: thesis:

per cases by A12, TARSKI:def 1, A11;

suppose A13: d = [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] -tree (t,s) ; :: thesis:

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 by A15, A13, TREES_3:def 15;

suppose A16: a = {} ; :: thesis:

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:

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:

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 by NAT_1:23, A22, A14;

suppose A23: n = 0 ; :: thesis:

then reconsider f = f as Element of dom t by A22;
A24: Vtree a = Vtree f by A13, A23, Th11, A22;
not a in Leaves (dom d) by A6, XBOOLE_0:def 5;
then A25: not f in Leaves (dom t) by A23, BINTREE1:6, A15, A13, A22;
then A26: f in (dom t) \ (Leaves (dom t)) by XBOOLE_0:def 5;
A27: t in Tseq . i by A10, A9, XBOOLE_0:def 5;
dom t is binary by BINTREE1:def 3;
then A28: succ f = {(f ^ <*0*>),(f ^ <*1*>)} by A25;
f ^ <*0*> in {(f ^ <*0*>),(f ^ <*1*>)} by TARSKI:def 2;
then reconsider b1 = f ^ <*0*> as Element of dom t by A28;
f ^ <*1*> in {(f ^ <*0*>),(f ^ <*1*>)} by TARSKI:def 2;
then reconsider c1 = f ^ <*1*> as Element of dom t by A28;
A29: Vtree f = (Vtree b1) + (Vtree c1) by A8, A4, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A26, A27;
A30: b = <*0*> ^ b1 by FINSEQ_1:32, A6, A23, A22;
A31: Vtree b = Vtree b1 by A13, A30, Th11;
c = <*0*> ^ c1 by FINSEQ_1:32, A6, A23, A22;
hence Vtree a = (Vtree b) + (Vtree c) by A24, A29, A31, A13, Th11; :: thesis:

end;

suppose A32: n = 1 ; :: thesis:

then reconsider f = f as Element of dom s by A22;
not a in Leaves (dom d) by A6, XBOOLE_0:def 5;
then A33: not f in Leaves (dom s) by A32, A22, BINTREE1:6, A15, A13;
then A34: f in (dom s) \ (Leaves (dom s)) by XBOOLE_0:def 5;
dom s is binary by BINTREE1:def 3;
then A35: succ f = {(f ^ <*0*>),(f ^ <*1*>)} by A33;
f ^ <*0*> in {(f ^ <*0*>),(f ^ <*1*>)} by TARSKI:def 2;
then reconsider b1 = f ^ <*0*> as Element of dom s by A35;
f ^ <*1*> in {(f ^ <*0*>),(f ^ <*1*>)} by TARSKI:def 2;
then reconsider c1 = f ^ <*1*> as Element of dom s by A35;
A36: Vtree f = (Vtree b1) + (Vtree c1) by A10, A8, A4, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A34, A9;
A37: b = <*1*> ^ b1 by FINSEQ_1:32, A6, A32, A22;
A38: Vtree b = Vtree b1 by A13, A37, Th12;
c = <*1*> ^ c1 by FINSEQ_1:32, A6, A32, A22;
then Vtree c = Vtree c1 by A13, Th12;
hence Vtree a = (Vtree b) + (Vtree c) by A13, A32, A22, Th12, A36, A38; :: thesis:

end;

suppose A39: d = [((MaxVl X) + 1),((Vrootr s) + (Vrootr t))] -tree (s,t) ; :: thesis:

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 by A41, A39, TREES_3:def 15;

suppose A42: a = {} ; :: thesis:

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:

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:

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 by NAT_1:23, A48, A40;

suppose A49: n = 0 ; :: thesis:

then reconsider f = f as Element of dom s by A48;
A50: Vtree a = Vtree f by A39, A49, Th11, A48;
not a in Leaves (dom d) by A6, XBOOLE_0:def 5;
then A51: not f in Leaves (dom s) by A49, BINTREE1:6, A41, A39, A48;
then A52: f in (dom s) \ (Leaves (dom s)) by XBOOLE_0:def 5;
dom s is binary by BINTREE1:def 3;
then A53: succ f = {(f ^ <*0*>),(f ^ <*1*>)} by A51;
f ^ <*0*> in {(f ^ <*0*>),(f ^ <*1*>)} by TARSKI:def 2;
then reconsider b1 = f ^ <*0*> as Element of dom s by A53;
f ^ <*1*> in {(f ^ <*0*>),(f ^ <*1*>)} by TARSKI:def 2;
then reconsider c1 = f ^ <*1*> as Element of dom s by A53;
A54: Vtree f = (Vtree b1) + (Vtree c1) by A10, A8, A4, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A52, A9;
A55: b = <*0*> ^ b1 by FINSEQ_1:32, A6, A49, A48;
A56: Vtree b = Vtree b1 by A39, A55, Th11;
c = <*0*> ^ c1 by FINSEQ_1:32, A6, A49, A48;
hence Vtree a = (Vtree b) + (Vtree c) by A50, A54, A56, A39, Th11; :: thesis:

end;

suppose A57: n = 1 ; :: thesis:

then reconsider f = f as Element of dom t by A48;
A58: Vtree a = Vtree f by A39, A57, Th12, A48;
not a in Leaves (dom d) by A6, XBOOLE_0:def 5;
then A59: not f in Leaves (dom t) by A57, BINTREE1:6, A41, A39, A48;
then A60: f in (dom t) \ (Leaves (dom t)) by XBOOLE_0:def 5;
A61: t in Tseq . i by A10, A9, XBOOLE_0:def 5;
dom t is binary by BINTREE1:def 3;
then A62: succ f = {(f ^ <*0*>),(f ^ <*1*>)} by A59;
f ^ <*0*> in {(f ^ <*0*>),(f ^ <*1*>)} by TARSKI:def 2;
then reconsider b1 = f ^ <*0*> as Element of dom t by A62;
f ^ <*1*> in {(f ^ <*0*>),(f ^ <*1*>)} by TARSKI:def 2;
then reconsider c1 = f ^ <*1*> as Element of dom t by A62;
A63: Vtree f = (Vtree b1) + (Vtree c1) by A8, A4, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A60, A61;
A64: b = <*1*> ^ b1 by FINSEQ_1:32, A6, A57, A48;
A65: Vtree b = Vtree b1 by A39, A64, Th12;
c = <*1*> ^ c1 by FINSEQ_1:32, A6, A57, A48;
hence Vtree a = (Vtree b) + (Vtree c) by A58, A63, A65, A39, Th12; :: thesis:

end;

A66: for i being Nat holds S₂[i] from NAT_1:sch 2(A2, A3);
let i be Nat; :: thesis:
let T be finite binary DecoratedTree of IndexedREAL ; :: thesis:
let t, s, r be Element of dom T; :: thesis:
assume A67: T in Tseq . i ; :: thesis:
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: