let T, T1 be finite Tree; :: thesis: for p being Element of T holds (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)
let p be Element of T; :: thesis: (card (T with-replacement (p,T1))) + (card (T | p)) = (card T) + (card T1)
defpred S1[ Element of T] means not p is_a_prefix_of \$1;
defpred S2[ Element of T] means p is_a_prefix_of \$1;
set A = { t where t is Element of T : S1[t] } ;
set B = { t where t is Element of T : S2[t] } ;
set C = { (p ^ t1) where t1 is Element of T1 : verum } ;
A1: { t where t is Element of T : S1[t] } is Subset of T from A2: { t where t is Element of T : S2[t] } is Subset of T from A3: T1, { (p ^ t1) where t1 is Element of T1 : verum } are_equipotent
proof
deffunc H1( Element of T1) -> FinSequence of NAT = p ^ \$1;
consider f being Function such that
A4: dom f = T1 and
A5: for n being Element of T1 holds f . n = H1(n) from take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = T1 & proj2 f = { (p ^ t1) where t1 is Element of T1 : verum } )
thus f is one-to-one :: thesis: ( proj1 f = T1 & proj2 f = { (p ^ t1) where t1 is Element of T1 : verum } )
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A6: ( x in dom f & y in dom f ) and
A7: f . x = f . y ; :: thesis: x = y
reconsider m = x, n = y as Element of T1 by A4, A6;
p ^ m = f . n by A5, A7
.= p ^ n by A5 ;
hence x = y by FINSEQ_1:33; :: thesis: verum
end;
thus dom f = T1 by A4; :: thesis: proj2 f = { (p ^ t1) where t1 is Element of T1 : verum }
thus rng f c= { (p ^ t1) where t1 is Element of T1 : verum } :: according to XBOOLE_0:def 10 :: thesis: { (p ^ t1) where t1 is Element of T1 : verum } c= proj2 f
proof
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng f or i in { (p ^ t1) where t1 is Element of T1 : verum } )
assume i in rng f ; :: thesis: i in { (p ^ t1) where t1 is Element of T1 : verum }
then consider n being object such that
A8: n in dom f and
A9: i = f . n by FUNCT_1:def 3;
T1 c= NAT * by TREES_1:def 3;
then reconsider n = n as Element of NAT * by A4, A8;
f . n = p ^ n by A4, A5, A8;
hence i in { (p ^ t1) where t1 is Element of T1 : verum } by A4, A8, A9; :: thesis: verum
end;
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in { (p ^ t1) where t1 is Element of T1 : verum } or i in proj2 f )
assume i in { (p ^ t1) where t1 is Element of T1 : verum } ; :: thesis: i in proj2 f
then consider n being Element of T1 such that
A10: i = p ^ n ;
i = f . n by ;
hence i in proj2 f by ; :: thesis: verum
end;
reconsider A = { t where t is Element of T : S1[t] } , B = { t where t is Element of T : S2[t] } as finite set by A1, A2;
now :: thesis: for x being object holds
( ( not x in T or x in A or x in B ) & ( ( x in A or x in B ) implies x in T ) )
let x be object ; :: thesis: ( ( not x in T or x in A or x in B ) & ( ( x in A or x in B ) implies x in T ) )
hereby :: thesis: ( ( x in A or x in B ) implies x in T )
assume x in T ; :: thesis: ( x in A or x in B )
then reconsider t = x as Element of T ;
( p is_a_prefix_of t or not p is_a_prefix_of t ) ;
hence ( x in A or x in B ) ; :: thesis: verum
end;
assume ( x in A or x in B ) ; :: thesis: x in T
hence x in T by A1, A2; :: thesis: verum
end;
then A11: T = A \/ B by XBOOLE_0:def 3;
A12: A misses { (p ^ t1) where t1 is Element of T1 : verum }
proof
assume not A misses { (p ^ t1) where t1 is Element of T1 : verum } ; :: thesis: contradiction
then consider x being object such that
A13: x in A /\ { (p ^ t1) where t1 is Element of T1 : verum } by XBOOLE_0:4;
x in { (p ^ t1) where t1 is Element of T1 : verum } by ;
then A14: ex t1 being Element of T1 st x = p ^ t1 ;
x in A by ;
then ex t being Element of T st
( x = t & not p is_a_prefix_of t ) ;
hence contradiction by A14, TREES_1:1; :: thesis: verum
end;
A15: A misses B
proof
assume not A misses B ; :: thesis: contradiction
then consider x being object such that
A16: x in A /\ B by XBOOLE_0:4;
x in B by ;
then A17: ex t being Element of T st
( x = t & p is_a_prefix_of t ) ;
x in A by ;
then ex t being Element of T st
( x = t & not p is_a_prefix_of t ) ;
hence contradiction by A17; :: thesis: verum
end;
A18: T with-replacement (p,T1) = A \/ { (p ^ t1) where t1 is Element of T1 : verum } by Th9;
reconsider C = { (p ^ t1) where t1 is Element of T1 : verum } as finite set by ;
A19: card T1 = card C by ;
T | p,B are_equipotent by Th8;
then card (T | p) = card B by CARD_1:5;
hence (card (T with-replacement (p,T1))) + (card (T | p)) = ((card A) + (card C)) + (card B) by
.= ((card A) + (card B)) + (card C)
.= (card T) + (card T1) by ;
:: thesis: verum