let T be full Tree; :: thesis: for n being Nat holds card (T -level n) = 2 to_power n
defpred S1[ Nat] means card (T -level $1) = 2 to_power $1;
A1: T = {0,1} * by Def2;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
defpred S2[ set , set ] means ex p being FinSequence st
( p = $1 & $2 = p ^ <*0*> );
let n be Nat; :: thesis: ( S1[n] implies 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 ) } ;
A3: (0* (n + 1)) . (n + 1) = 0 by FINSEQ_1:4, FUNCOP_1:7;
( len (0* (n + 1)) = n + 1 & 0* (n + 1) in T ) by A1, BINARI_3:4, CARD_1:def 7;
then A4: 0* (n + 1) in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } by A3;
A5: { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } c= T -level (n + 1)
proof
let x be object ; :: 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
A6: p = x and
A7: len p = n + 1 and
p . (n + 1) = 1 ;
p in { w where w is Element of T : len w = n + 1 } by A7;
hence x in T -level (n + 1) by A6, TREES_2:def 6; :: thesis: verum
end;
rng <*1*> c= {0,1}
proof
let z be object ; :: 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:38;
then z = 1 by TARSKI:def 1;
hence z in {0,1} by TARSKI:def 2; :: thesis: verum
end;
then A8: <*1*> is FinSequence of {0,1} by FINSEQ_1:def 4;
defpred S3[ set , set ] means ex p being FinSequence st
( p = $1 & $2 = p ^ <*1*> );
A9: { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 0 ) } c= T -level (n + 1)
proof
let x be object ; :: 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
A10: p = x and
A11: len p = n + 1 and
p . (n + 1) = 0 ;
p in { w where w is Element of T : len w = n + 1 } by A11;
hence x in T -level (n + 1) by A10, TREES_2:def 6; :: thesis: verum
end;
0* n in {0,1} * by BINARI_3:4;
then 0* n is FinSequence of {0,1} by FINSEQ_1:def 11;
then (0* n) ^ <*1*> is FinSequence of {0,1} by A8, Lm1;
then A12: (0* n) ^ <*1*> in T by A1, FINSEQ_1:def 11;
reconsider Tn = T -level n as non empty finite set by A1, Th10;
assume A13: card (T -level n) = 2 to_power n ; :: thesis: S1[n + 1]
len (0* n) = n by CARD_1:def 7;
then A14: ((0* n) ^ <*1*>) . (n + 1) = 1 by FINSEQ_1:42;
len ((0* n) ^ <*1*>) = (len (0* n)) + 1 by FINSEQ_2:16
.= n + 1 by CARD_1:def 7 ;
then (0* n) ^ <*1*> in { p where p is Element of T : ( len p = n + 1 & p . (n + 1) = 1 ) } by A12, A14;
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 A4, A9, A5;
A15: Tn10 \/ Tn11 c= T -level (n + 1) by A9, A5, XBOOLE_1:8;
A16: 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
A17: p = x and
A18: len p = n ;
set y = p ^ <*1*>;
p ^ <*1*> is FinSequence of {0,1} by A8, Lm1;
then A19: p ^ <*1*> in T by A1, FINSEQ_1:def 11;
( len (p ^ <*1*>) = n + 1 & (p ^ <*1*>) . (n + 1) = 1 ) by A18, FINSEQ_1:42, FINSEQ_2:16;
then p ^ <*1*> in { t where t is Element of T : ( len t = n + 1 & t . (n + 1) = 1 ) } by A19;
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 A17; :: thesis: verum
end;
consider f1 being Function of Tn,Tn11 such that
A20: for x being Element of Tn holds S3[x,f1 . x] from FUNCT_2:sch 3(A16);
now :: thesis: for y being object st y in Tn11 holds
ex x being object st
( x in Tn & y = f1 . x )
let y be object ; :: thesis: ( y in Tn11 implies ex x being object st
( x in Tn & y = f1 . x ) )
assume y in Tn11 ; :: thesis: ex x being object st
( x in Tn & y = f1 . x )
then consider t being Element of T such that
A21: t = y and
A22: len t = n + 1 and
A23: t . (n + 1) = 1 ;
consider p being FinSequence of BOOLEAN , d being Element of BOOLEAN such that
A24: t = p ^ <*d*> by A22, FINSEQ_2:19;
reconsider x = p as object ;
take x = x; :: thesis: ( x in Tn & y = f1 . x )
A25: (len p) + 1 = n + 1 by A22, A24, FINSEQ_2:16;
p in T by A1, FINSEQ_1:def 11;
then A26: p in { w where w is Element of T : len w = n } by A25;
hence x in Tn by TREES_2:def 6; :: thesis: y = f1 . x
reconsider x9 = x as Element of Tn by A26, TREES_2:def 6;
ex q being FinSequence st
( q = x9 & f1 . x9 = q ^ <*1*> ) by A20;
hence y = f1 . x by A21, A23, A24, A25, FINSEQ_1:42; :: thesis: verum
end;
then A27: rng f1 = Tn11 by FUNCT_2:10;
A28: 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
A29: p = x and
A30: len p = n ;
set y = p ^ <*0*>;
rng <*0*> c= {0,1}
proof
let z be object ; :: 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:38;
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 A31: p ^ <*0*> in T by A1, FINSEQ_1:def 11;
( len (p ^ <*0*>) = n + 1 & (p ^ <*0*>) . (n + 1) = 0 ) by A30, FINSEQ_1:42, FINSEQ_2:16;
then p ^ <*0*> in { t where t is Element of T : ( len t = n + 1 & t . (n + 1) = 0 ) } by A31;
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 A29; :: thesis: verum
end;
consider f0 being Function of Tn,Tn10 such that
A32: for x being Element of Tn holds S2[x,f0 . x] from FUNCT_2:sch 3(A28);
now :: thesis: for x1, x2 being object st x1 in dom f1 & x2 in dom f1 & f1 . x1 = f1 . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom f1 & x2 in dom f1 & f1 . x1 = f1 . x2 implies x1 = x2 )
assume that
A33: ( x1 in dom f1 & x2 in dom f1 ) and
A34: f1 . x1 = f1 . x2 ; :: thesis: x1 = x2
reconsider x19 = x1, x29 = x2 as Element of Tn by A33, FUNCT_2:def 1;
( ex p1 being FinSequence st
( p1 = x19 & f1 . x19 = p1 ^ <*1*> ) & ex p2 being FinSequence st
( p2 = x29 & f1 . x29 = p2 ^ <*1*> ) ) by A20;
hence x1 = x2 by A34, FINSEQ_2:17; :: thesis: verum
end;
then ( Tn c= dom f1 & f1 is one-to-one ) by FUNCT_1:def 4, FUNCT_2:def 1;
then Tn,f1 .: Tn are_equipotent by CARD_1:33;
then A35: Tn, rng f1 are_equipotent by RELSET_1:22;
A36: T -level (n + 1) c= Tn10 \/ Tn11
proof
let x be object ; :: 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
A37: p = x and
A38: len p = n + 1 ;
( x in Tn10 or x in Tn11 )
proof
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in dom p by A38, FINSEQ_1:def 3;
then p . (n + 1) in BOOLEAN by FINSEQ_2:11;
then A39: ( p . (n + 1) = 0 or p . (n + 1) = 1 ) by TARSKI:def 2;
assume not x in Tn10 ; :: thesis: x in Tn11
hence x in Tn11 by A37, A38, A39; :: thesis: verum
end;
hence x in Tn10 \/ Tn11 by XBOOLE_0:def 3; :: thesis: verum
end;
now :: thesis: for y being object st y in Tn10 holds
ex x being object st
( x in Tn & y = f0 . x )
let y be object ; :: thesis: ( y in Tn10 implies ex x being object st
( x in Tn & y = f0 . x ) )
assume y in Tn10 ; :: thesis: ex x being object st
( x in Tn & y = f0 . x )
then consider t being Element of T such that
A40: t = y and
A41: len t = n + 1 and
A42: t . (n + 1) = 0 ;
consider p being FinSequence of BOOLEAN , d being Element of BOOLEAN such that
A43: t = p ^ <*d*> by A41, FINSEQ_2:19;
reconsider x = p as object ;
take x = x; :: thesis: ( x in Tn & y = f0 . x )
A44: (len p) + 1 = n + 1 by A41, A43, FINSEQ_2:16;
p in T by A1, FINSEQ_1:def 11;
then A45: p in { w where w is Element of T : len w = n } by A44;
hence x in Tn by TREES_2:def 6; :: thesis: y = f0 . x
reconsider x9 = x as Element of Tn by A45, TREES_2:def 6;
ex q being FinSequence st
( q = x9 & f0 . x9 = q ^ <*0*> ) by A32;
hence y = f0 . x by A40, A42, A43, A44, FINSEQ_1:42; :: thesis: verum
end;
then A46: rng f0 = Tn10 by FUNCT_2:10;
now :: thesis: for x1, x2 being object st x1 in dom f0 & x2 in dom f0 & f0 . x1 = f0 . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom f0 & x2 in dom f0 & f0 . x1 = f0 . x2 implies x1 = x2 )
assume that
A47: ( x1 in dom f0 & x2 in dom f0 ) and
A48: f0 . x1 = f0 . x2 ; :: thesis: x1 = x2
reconsider x19 = x1, x29 = x2 as Element of Tn by A47, FUNCT_2:def 1;
( ex p1 being FinSequence st
( p1 = x19 & f0 . x19 = p1 ^ <*0*> ) & ex p2 being FinSequence st
( p2 = x29 & f0 . x29 = p2 ^ <*0*> ) ) by A32;
hence x1 = x2 by A48, FINSEQ_2:17; :: thesis: verum
end;
then ( Tn c= dom f0 & f0 is one-to-one ) by FUNCT_1:def 4, FUNCT_2:def 1;
then Tn,f0 .: Tn are_equipotent by CARD_1:33;
then Tn, rng f0 are_equipotent by RELSET_1:22;
then A49: card Tn = card Tn10 by A46, CARD_1:5;
A50: Tn10 misses Tn11
proof
assume Tn10 /\ Tn11 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being object such that
A51: x in Tn10 /\ Tn11 by XBOOLE_0:def 1;
x in Tn11 by A51, XBOOLE_0:def 4;
then A52: ex p2 being Element of T st
( p2 = x & len p2 = n + 1 & p2 . (n + 1) = 1 ) ;
x in Tn10 by A51, XBOOLE_0:def 4;
then ex p1 being Element of T st
( p1 = x & len p1 = n + 1 & p1 . (n + 1) = 0 ) ;
hence contradiction by A52; :: thesis: verum
end;
thus 2 to_power (n + 1) = (2 to_power n) * (2 to_power 1) by POWER:27
.= 2 * (2 to_power n) by POWER:25
.= (card Tn) + (card Tn) by A13
.= (card Tn10) + (card Tn11) by A49, A35, A27, CARD_1:5
.= card (Tn10 \/ Tn11) by A50, CARD_2:40
.= card (T -level (n + 1)) by A15, A36, XBOOLE_0:def 10 ; :: thesis: verum
end;
card (T -level 0) = card {{}} by TREES_9:44
.= 1 by CARD_1:30
.= 2 to_power 0 by POWER:24 ;
then A53: S1[ 0 ] ;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A53, A2); :: thesis: verum