let T be full Tree; :: thesis: for n being Element of NAT holds card (T -level n) = 2 to_power n
A1: T = {0 ,1} * by Def2;
defpred S1[ Element of NAT ] means card (T -level $1) = 2 to_power $1;
card (T -level 0 ) = card {{} } by QC_LANG4:17
.= 1 by CARD_1:50
.= 2 to_power 0 by POWER:29 ;
then A2: S1[ 0 ] ;
A3: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: card (T -level n) = 2 to_power n ; :: thesis: S1[n + 1]
set Tn10 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } ;
set Tn11 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } ;
A5: len (0* (n + 1)) = n + 1 by FINSEQ_1:def 18;
A6: 0* (n + 1) in T by A1, BINARI_3:5;
(0* (n + 1)) . (n + 1) = 0 by FINSEQ_1:6, FUNCOP_1:13;
then A7: 0* (n + 1) in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } by A5, A6;
A8: len ((0* n) ^ <*1*>) = (len (0* n)) + 1 by FINSEQ_2:19
.= n + 1 by FINSEQ_1:def 18 ;
0* n in {0 ,1} * by BINARI_3:5;
then A9: 0* n is FinSequence of {0 ,1} by FINSEQ_1:def 11;
rng <*1*> c= {0 ,1}
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*1*> or z in {0 ,1} )
assume z in rng <*1*> ; :: thesis: z in {0 ,1}
then z in {1} by FINSEQ_1:55;
then z = 1 by TARSKI:def 1;
hence z in {0 ,1} by TARSKI:def 2; :: thesis: verum
end;
then A10: <*1*> is FinSequence of {0 ,1} by FINSEQ_1:def 4;
then (0* n) ^ <*1*> is FinSequence of {0 ,1} by A9, Lm1;
then A11: (0* n) ^ <*1*> in T by A1, FINSEQ_1:def 11;
len (0* n) = n by FINSEQ_1:def 18;
then ((0* n) ^ <*1*>) . (n + 1) = 1 by FINSEQ_1:59;
then A12: (0* n) ^ <*1*> in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } by A8, A11;
A13: { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } c= T -level (n + 1)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } or x in T -level (n + 1) )
assume x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } ; :: thesis: x in T -level (n + 1)
then consider p being Element of T such that
A14: p = x and
A15: len p = n + 1 and
p . (n + 1) = 0 ;
p in { w where w is Element of T : len w = n + 1 } by A15;
hence x in T -level (n + 1) by A14, TREES_2:def 6; :: thesis: verum
end;
A16: { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } c= T -level (n + 1)
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } or x in T -level (n + 1) )
assume x in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } ; :: thesis: x in T -level (n + 1)
then consider p being Element of T such that
A17: p = x and
A18: len p = n + 1 and
p . (n + 1) = 1 ;
p in { w where w is Element of T : len w = n + 1 } by A18;
hence x in T -level (n + 1) by A17, TREES_2:def 6; :: thesis: verum
end;
then reconsider Tn10 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } , Tn11 = { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } as non empty finite set by A7, A12, A13;
A19: Tn10 \/ Tn11 c= T -level (n + 1) by A13, A16, XBOOLE_1:8;
A20: T -level (n + 1) c= Tn10 \/ Tn11
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T -level (n + 1) or x in Tn10 \/ Tn11 )
assume x in T -level (n + 1) ; :: thesis: x in Tn10 \/ Tn11
then x in { w where w is Element of T : len w = n + 1 } by TREES_2:def 6;
then consider p being Element of T such that
A21: p = x and
A22: len p = n + 1 ;
( x in Tn10 or x in Tn11 )
proof
assume A23: not x in Tn10 ; :: thesis: x in Tn11
n + 1 in Seg (n + 1) by FINSEQ_1:6;
then n + 1 in dom p by A22, FINSEQ_1:def 3;
then p . (n + 1) in BOOLEAN by FINSEQ_2:13;
then ( p . (n + 1) = 0 or p . (n + 1) = 1 ) by TARSKI:def 2;
hence x in Tn11 by A21, A22, A23; :: thesis: verum
end;
hence x in Tn10 \/ Tn11 by XBOOLE_0:def 3; :: thesis: verum
end;
A24: Tn10 misses Tn11
proof
assume Tn10 /\ Tn11 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being set such that
A25: x in Tn10 /\ Tn11 by XBOOLE_0:def 1;
A26: ( x in Tn10 & x in Tn11 ) by A25, XBOOLE_0:def 4;
then consider p1 being Element of T such that
A27: p1 = x and
len p1 = n + 1 and
A28: p1 . (n + 1) = 0 ;
consider p2 being Element of T such that
A29: p2 = x and
len p2 = n + 1 and
A30: p2 . (n + 1) = 1 by A26;
thus contradiction by A27, A28, A29, A30; :: thesis: verum
end;
reconsider Tn = T -level n as non empty finite set by A1, Th10;
defpred S2[ set , set ] means ex p being FinSequence st
( p = $1 & $2 = p ^ <*0 *> );
A31: for x being Element of Tn ex y being Element of Tn10 st S2[x,y]
proof
let x be Element of Tn; :: thesis: ex y being Element of Tn10 st S2[x,y]
x in T -level n ;
then x in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider p being Element of T such that
A32: p = x and
A33: len p = n ;
set y = p ^ <*0 *>;
rng <*0 *> c= {0 ,1}
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*0 *> or z in {0 ,1} )
assume z in rng <*0 *> ; :: thesis: z in {0 ,1}
then z in {0 } by FINSEQ_1:55;
then z = 0 by TARSKI:def 1;
hence z in {0 ,1} by TARSKI:def 2; :: thesis: verum
end;
then <*0 *> is FinSequence of {0 ,1} by FINSEQ_1:def 4;
then p ^ <*0 *> is FinSequence of {0 ,1} by Lm1;
then A34: p ^ <*0 *> in T by A1, FINSEQ_1:def 11;
A35: len (p ^ <*0 *>) = n + 1 by A33, FINSEQ_2:19;
(p ^ <*0 *>) . (n + 1) = 0 by A33, FINSEQ_1:59;
then p ^ <*0 *> in { t where t is Element of T : ( len t = n + 1 & t . (n + 1) = 0 ) } by A34, A35;
then reconsider y = p ^ <*0 *> as Element of Tn10 ;
take y ; :: thesis: S2[x,y]
take p ; :: thesis: ( p = x & y = p ^ <*0 *> )
thus ( p = x & y = p ^ <*0 *> ) by A32; :: thesis: verum
end;
defpred S3[ set , set ] means ex p being FinSequence st
( p = $1 & $2 = p ^ <*1*> );
A36: for x being Element of Tn ex y being Element of Tn11 st S3[x,y]
proof
let x be Element of Tn; :: thesis: ex y being Element of Tn11 st S3[x,y]
x in T -level n ;
then x in { w where w is Element of T : len w = n } by TREES_2:def 6;
then consider p being Element of T such that
A37: p = x and
A38: len p = n ;
set y = p ^ <*1*>;
p ^ <*1*> is FinSequence of {0 ,1} by A10, Lm1;
then A39: p ^ <*1*> in T by A1, FINSEQ_1:def 11;
A40: len (p ^ <*1*>) = n + 1 by A38, FINSEQ_2:19;
(p ^ <*1*>) . (n + 1) = 1 by A38, FINSEQ_1:59;
then p ^ <*1*> in { t where t is Element of T : ( len t = n + 1 & t . (n + 1) = 1 ) } by A39, A40;
then reconsider y = p ^ <*1*> as Element of Tn11 ;
take y ; :: thesis: S3[x,y]
take p ; :: thesis: ( p = x & y = p ^ <*1*> )
thus ( p = x & y = p ^ <*1*> ) by A37; :: thesis: verum
end;
consider f0 being Function of Tn,Tn10 such that
A41: for x being Element of Tn holds S2[x,f0 . x] from FUNCT_2:sch 3(A31);
 consider f1 being Function of Tn,Tn11 such that
A42: for x being Element of Tn holds S3[x,f1 . x] from FUNCT_2:sch 3(A36);
 A43: Tn c= dom f0 by FUNCT_2:def 1;
now
let x1, x2 be set ; :: thesis: ( x1 in dom f0 & x2 in dom f0 & f0 . x1 = f0 . x2 implies x1 = x2 )
assume that
A44: x1 in dom f0 and
A45: x2 in dom f0 and
A46: f0 . x1 = f0 . x2 ; :: thesis: x1 = x2
reconsider x1' = x1, x2' = x2 as Element of Tn by A44, A45, FUNCT_2:def 1;
consider p1 being FinSequence such that
A47: p1 = x1' and
A48: f0 . x1' = p1 ^ <*0 *> by A41;
consider p2 being FinSequence such that
A49: p2 = x2' and
A50: f0 . x2' = p2 ^ <*0 *> by A41;
thus x1 = x2 by A46, A47, A48, A49, A50, FINSEQ_2:20; :: thesis: verum
end;
then f0 is one-to-one by FUNCT_1:def 8;
then Tn,f0 .: Tn are_equipotent by A43, CARD_1:60;
then A51: Tn, rng f0 are_equipotent by FUNCT_2:45;
now
let y be set ; :: thesis: ( y in Tn10 implies ex x being set st
( x in Tn & y = f0 . x ) )
assume y in Tn10 ; :: thesis: ex x being set st
( x in Tn & y = f0 . x )
then consider t being Element of T such that
A52: t = y and
A53: len t = n + 1 and
A54: t . (n + 1) = 0 ;
consider p being FinSequence of BOOLEAN , d being Element of BOOLEAN such that
A55: t = p ^ <*d*> by A53, FINSEQ_2:22;
A56: (len p) + 1 = n + 1 by A53, A55, FINSEQ_2:19;
reconsider x = p as set ;
take x = x; :: thesis: ( x in Tn & y = f0 . x )
p in T by A1, FINSEQ_1:def 11;
then A57: p in { w where w is Element of T : len w = n } by A56;
hence x in Tn by TREES_2:def 6; :: thesis: y = f0 . x
reconsider x' = x as Element of Tn by A57, TREES_2:def 6;
consider q being FinSequence such that
A58: q = x' and
A59: f0 . x' = q ^ <*0 *> by A41;
thus y = f0 . x by A52, A54, A55, A56, A58, A59, FINSEQ_1:59; :: thesis: verum
end;
then rng f0 = Tn10 by FUNCT_2:16;
then A60: card Tn = card Tn10 by A51, CARD_1:21;
A61: Tn c= dom f1 by FUNCT_2:def 1;
now
let x1, x2 be set ; :: thesis: ( x1 in dom f1 & x2 in dom f1 & f1 . x1 = f1 . x2 implies x1 = x2 )
assume that
A62: x1 in dom f1 and
A63: x2 in dom f1 and
A64: f1 . x1 = f1 . x2 ; :: thesis: x1 = x2
reconsider x1' = x1, x2' = x2 as Element of Tn by A62, A63, FUNCT_2:def 1;
consider p1 being FinSequence such that
A65: p1 = x1' and
A66: f1 . x1' = p1 ^ <*1*> by A42;
consider p2 being FinSequence such that
A67: p2 = x2' and
A68: f1 . x2' = p2 ^ <*1*> by A42;
thus x1 = x2 by A64, A65, A66, A67, A68, FINSEQ_2:20; :: thesis: verum
end;
then f1 is one-to-one by FUNCT_1:def 8;
then Tn,f1 .: Tn are_equipotent by A61, CARD_1:60;
then A69: Tn, rng f1 are_equipotent by FUNCT_2:45;
now
let y be set ; :: thesis: ( y in Tn11 implies ex x being set st
( x in Tn & y = f1 . x ) )
assume y in Tn11 ; :: thesis: ex x being set st
( x in Tn & y = f1 . x )
then consider t being Element of T such that
A70: t = y and
A71: len t = n + 1 and
A72: t . (n + 1) = 1 ;
consider p being FinSequence of BOOLEAN , d being Element of BOOLEAN such that
A73: t = p ^ <*d*> by A71, FINSEQ_2:22;
A74: (len p) + 1 = n + 1 by A71, A73, FINSEQ_2:19;
reconsider x = p as set ;
take x = x; :: thesis: ( x in Tn & y = f1 . x )
p in T by A1, FINSEQ_1:def 11;
then A75: p in { w where w is Element of T : len w = n } by A74;
hence x in Tn by TREES_2:def 6; :: thesis: y = f1 . x
reconsider x' = x as Element of Tn by A75, TREES_2:def 6;
consider q being FinSequence such that
A76: q = x' and
A77: f1 . x' = q ^ <*1*> by A42;
thus y = f1 . x by A70, A72, A73, A74, A76, A77, FINSEQ_1:59; :: thesis: verum
end;
then A78: rng f1 = Tn11 by FUNCT_2:16;
thus 2 to_power (n + 1) = (2 to_power n) * (2 to_power 1) by POWER:32
.= 2 * (2 to_power n) by POWER:30
.= (card Tn) + (card Tn) by A4
.= (card Tn10) + (card Tn11) by A60, A69, A78, CARD_1:21
.= card (Tn10 \/ Tn11) by A24, CARD_2:53
.= card (T -level (n + 1)) by A19, A20, XBOOLE_0:def 10 ; :: thesis: verum
end;
thus for n being Element of NAT holds S1[n] from NAT_1:sch 1(A2, A3); :: thesis: verum