let IAlph, OAlph be non empty set ; :: thesis:
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis:
let CRtfsm1, CRtfsm2 be non empty finite reduced connected Mealy-FSM of IAlph,OAlph; :: thesis:
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
assume A1: ( the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,CRtfsm2 -are_equivalent & tfsm = CRtfsm1 -Mealy_union CRtfsm2 ) ; :: thesis:
assume ex Q being State of (the_reduction_of tfsm) st
for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm1 or not q2 in the carrier of CRtfsm2 or ex q being Element of Q st
( not q = q1 & not q = q2 ) ) ; :: thesis:
then consider Q being Element of (the_reduction_of tfsm) such that
A2: for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm1 or not q2 in the carrier of CRtfsm2 or ex q being Element of Q st
( not q = q1 & not q = q2 ) ) ;
A3: the carrier of CRtfsm1 /\ the carrier of CRtfsm2 = {} by A1, XBOOLE_0:def 7;
set rtfsm = the_reduction_of tfsm;
set Srtfsm1 = the carrier of CRtfsm1;
set ISrtfsm1 = the InitS of CRtfsm1;
set Srtfsm2 = the carrier of CRtfsm2;
set ISrtfsm2 = the InitS of CRtfsm2;
set Stfsm = the carrier of tfsm;
set Srtfsm = the carrier of (the_reduction_of tfsm);
A4: the carrier of (the_reduction_of tfsm) = final_states_partition tfsm by Def18;
then reconsider Q = Q as Subset of the carrier of tfsm by TARSKI:def 3;
Q in the carrier of (the_reduction_of tfsm) ;
then A5: Q in final_states_partition tfsm by Def18;
then A6: Q <> {} by EQREL_1:def 6;
then consider q being Element of the carrier of tfsm such that
A7: q in Q by SUBSET_1:10;
union (final_states_partition tfsm) = the carrier of tfsm by EQREL_1:def 6
.= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A1, Def24 ;
then A8: Q c= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A4, ZFMISC_1:92;

per cases by A7, A8, XBOOLE_0:def 3;

suppose A9: q in the carrier of CRtfsm1 ; :: thesis:

set Q' = Q \ {q};

A10: now

assume A11: Q \ {q} = {} ; :: thesis:
reconsider q = q as Element of the carrier of CRtfsm1 by A9;
q is accessible by Def22;
then consider w being FinSequence of IAlph such that
A12: the InitS of CRtfsm1,w -leads_to q by Def21;
set adl = the InitS of CRtfsm2 leads_to_under w;

A13: now

assume A14: the InitS of CRtfsm2 leads_to_under w in Q ; :: thesis:
the InitS of CRtfsm2 leads_to_under w <> q by A3, XBOOLE_0:def 4;
hence contradiction by A11, A14, ZFMISC_1:64; :: thesis:

end;

now

assume A15: not the InitS of CRtfsm2 leads_to_under w in Q ; :: thesis:
A16: the InitS of CRtfsm2 leads_to_under w in the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by XBOOLE_0:def 3;
reconsider q = q as Element of the carrier of tfsm ;
reconsider adl = the InitS of CRtfsm2 leads_to_under w as Element of the carrier of tfsm by A1, A16, Def24;
A17: final_states_partition tfsm is final by Def15;
for Y being Element of the carrier of (the_reduction_of tfsm) holds
( not q in Y or not adl in Y )

proof

assume ex Y being Element of the carrier of (the_reduction_of tfsm) st
( q in Y & adl in Y ) ; :: thesis:
then consider Y being Element of the carrier of (the_reduction_of tfsm) such that
A18: ( q in Y & adl in Y ) ;
reconsider Y = Y as Subset of the carrier of tfsm by A4, TARSKI:def 3;
reconsider Q = Q as Subset of the carrier of tfsm ;
Y in the carrier of (the_reduction_of tfsm) ;
then Y in final_states_partition tfsm by Def18;
then Y misses Q by A5, A15, A18, EQREL_1:def 6;
hence contradiction by A7, A18, XBOOLE_0:3; :: thesis:

end;

then not q,adl -are_equivalent by A4, A17, Def14;
then consider dseq being FinSequence of IAlph such that
A19: q,dseq -response <> adl,dseq -response by Def10;
reconsider adl2 = adl as Element of the carrier of CRtfsm2 ;
reconsider q1 = q as Element of the carrier of CRtfsm1 ;
A20: the InitS of CRtfsm2,w -leads_to adl2 by Def5;
q,dseq -response = q1,dseq -response by A1, Th72;
then q1,dseq -response <> adl2,dseq -response by A1, A19, Th74;
then the InitS of CRtfsm1,(w ^ dseq) -response <> the InitS of CRtfsm2,(w ^ dseq) -response by A12, A20, Th27;
hence contradiction by A1, Def9; :: thesis:

end;

hence contradiction by A13; :: thesis:

end;

now

assume A21: Q \ {q} <> {} ; :: thesis:
A22: Q \ {q} c= Q by XBOOLE_1:36;
reconsider Q = Q as Subset of the carrier of tfsm ;
reconsider Q' = Q \ {q} as Subset of the carrier of tfsm ;
consider x being Element of the carrier of tfsm such that
A23: x in Q' by A21, SUBSET_1:10;
A24: Q' c= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A8, A22, XBOOLE_1:1;

per cases by A23, A24, XBOOLE_0:def 3;

suppose A25: x in the carrier of CRtfsm1 ; :: thesis:

reconsider q = q as Element of Q by A7;
reconsider x = x as Element of Q by A23, XBOOLE_0:def 5;
( not q in the carrier of CRtfsm1 or not x in the carrier of CRtfsm1 or q = x ) by A1, Th78;
hence contradiction by A9, A23, A25, ZFMISC_1:64; :: thesis:

end;

suppose A26: x in the carrier of CRtfsm2 ; :: thesis:

set Q'' = Q' \ {x};

A27: now

assume A28: Q' \ {x} = {} ; :: thesis:
A29: for z being Element of Q holds
( z = q or z = x )

proof

given z being Element of Q such that A30: ( z <> q & z <> x ) ; :: thesis:
z in Q' by A6, A30, ZFMISC_1:64;
hence contradiction by A28, A30, ZFMISC_1:64; :: thesis:

end;

reconsider q = q as Element of Q by A7;
reconsider x = x as Element of Q by A23, ZFMISC_1:64;
( not q in the carrier of CRtfsm1 or not x in the carrier of CRtfsm2 or ex z being Element of Q st
( z <> q & z <> x ) ) by A2;
hence contradiction by A9, A26, A29; :: thesis:

end;

now

assume A31: Q' \ {x} <> {} ; :: thesis:
A32: Q' \ {x} c= Q' by XBOOLE_1:36;
reconsider Q' = Q' as Subset of the carrier of tfsm ;
reconsider Q'' = Q' \ {x} as Subset of the carrier of tfsm ;
consider y being Element of the carrier of tfsm such that
A33: y in Q'' by A31, SUBSET_1:10;
A34: Q'' c= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A24, A32, XBOOLE_1:1;

per cases by A33, A34, XBOOLE_0:def 3;

suppose A35: y in the carrier of CRtfsm1 ; :: thesis:

A36: y in Q' by A33, ZFMISC_1:64;
reconsider q = q as Element of Q by A7;
reconsider y = y as Element of Q by A36, ZFMISC_1:64;
( not q in the carrier of CRtfsm1 or not y in the carrier of CRtfsm1 or q = y ) by A1, Th78;
hence contradiction by A9, A35, A36, ZFMISC_1:64; :: thesis:

end;

suppose A37: y in the carrier of CRtfsm2 ; :: thesis:

reconsider x = x as Element of Q by A23, ZFMISC_1:64;
y in Q' by A33, ZFMISC_1:64;
then reconsider y = y as Element of Q by ZFMISC_1:64;
( not x in the carrier of CRtfsm2 or not y in the carrier of CRtfsm2 or x = y ) by A1, Th79;
hence contradiction by A26, A33, A37, ZFMISC_1:64; :: thesis:

end;

hence contradiction by A27; :: thesis:

end;

hence contradiction by A10; :: thesis:

end;

suppose A38: q in the carrier of CRtfsm2 ; :: thesis:

set Q' = Q \ {q};

A39: now

assume A40: Q \ {q} = {} ; :: thesis:
reconsider q = q as Element of the carrier of CRtfsm2 by A38;
q is accessible by Def22;
then consider w being FinSequence of IAlph such that
A41: the InitS of CRtfsm2,w -leads_to q by Def21;
set adl = the InitS of CRtfsm1 leads_to_under w;

A42: now

assume A43: the InitS of CRtfsm1 leads_to_under w in Q ; :: thesis:
the InitS of CRtfsm1 leads_to_under w <> q by A1, XBOOLE_0:3;
hence contradiction by A40, A43, ZFMISC_1:64; :: thesis:

end;

now

assume A44: not the InitS of CRtfsm1 leads_to_under w in Q ; :: thesis:
A45: the InitS of CRtfsm1 leads_to_under w in the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by XBOOLE_0:def 3;
reconsider q = q as Element of the carrier of tfsm ;
reconsider adl = the InitS of CRtfsm1 leads_to_under w as Element of the carrier of tfsm by A1, A45, Def24;
A46: final_states_partition tfsm is final by Def15;
for Y being Element of the carrier of (the_reduction_of tfsm) holds
( not q in Y or not adl in Y )

proof

assume ex Y being Element of the carrier of (the_reduction_of tfsm) st
( q in Y & adl in Y ) ; :: thesis:
then consider Y being Element of the carrier of (the_reduction_of tfsm) such that
A47: ( q in Y & adl in Y ) ;
reconsider Y = Y as Subset of the carrier of tfsm by A4, TARSKI:def 3;
Y in the carrier of (the_reduction_of tfsm) ;
then Y in final_states_partition tfsm by Def18;
then Y misses Q by A5, A44, A47, EQREL_1:def 6;
hence contradiction by A7, A47, XBOOLE_0:3; :: thesis:

end;

then not q,adl -are_equivalent by A4, A46, Def14;
then consider dseq being FinSequence of IAlph such that
A48: q,dseq -response <> adl,dseq -response by Def10;
reconsider adl2 = adl as Element of the carrier of CRtfsm1 ;
reconsider q1 = q as Element of the carrier of CRtfsm2 ;
A49: the InitS of CRtfsm1,w -leads_to adl2 by Def5;
q,dseq -response = q1,dseq -response by A1, Th74;
then q1,dseq -response <> adl2,dseq -response by A1, A48, Th72;
then the InitS of CRtfsm2,(w ^ dseq) -response <> the InitS of CRtfsm1,(w ^ dseq) -response by A41, A49, Th27;
hence contradiction by A1, Def9; :: thesis:

end;

hence contradiction by A42; :: thesis:

end;

now

assume A50: Q \ {q} <> {} ; :: thesis:
A51: Q \ {q} c= Q by XBOOLE_1:36;
reconsider Q = Q as Subset of the carrier of tfsm ;
reconsider Q' = Q \ {q} as Subset of the carrier of tfsm ;
consider x being Element of the carrier of tfsm such that
A52: x in Q' by A50, SUBSET_1:10;
A53: Q' c= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A8, A51, XBOOLE_1:1;

per cases by A52, A53, XBOOLE_0:def 3;

suppose A54: x in the carrier of CRtfsm1 ; :: thesis:

set Q'' = Q' \ {x};

A55: now

assume A56: Q' \ {x} = {} ; :: thesis:
A57: for z being Element of Q holds
( z = q or z = x )

proof

given z being Element of Q such that A58: ( z <> q & z <> x ) ; :: thesis:
z in Q' by A6, A58, ZFMISC_1:64;
hence contradiction by A56, A58, ZFMISC_1:64; :: thesis:

end;

reconsider q = q as Element of Q by A7;
reconsider x = x as Element of Q by A52, ZFMISC_1:64;
( not x in the carrier of CRtfsm1 or not q in the carrier of CRtfsm2 or ex z being Element of Q st
( z <> x & z <> q ) ) by A2;
hence contradiction by A38, A54, A57; :: thesis:

end;

now

assume A59: Q' \ {x} <> {} ; :: thesis:
A60: Q' \ {x} c= Q' by XBOOLE_1:36;
reconsider Q' = Q' as Subset of the carrier of tfsm ;
reconsider Q'' = Q' \ {x} as Subset of the carrier of tfsm ;
consider y being Element of the carrier of tfsm such that
A61: y in Q'' by A59, SUBSET_1:10;
A62: Q'' c= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A53, A60, XBOOLE_1:1;

per cases by A61, A62, XBOOLE_0:def 3;

suppose A63: y in the carrier of CRtfsm1 ; :: thesis:

reconsider x = x as Element of Q by A52, ZFMISC_1:64;
y in Q' by A61, ZFMISC_1:64;
then reconsider y = y as Element of Q by ZFMISC_1:64;
( not x in the carrier of CRtfsm1 or not y in the carrier of CRtfsm1 or x = y ) by A1, Th78;
hence contradiction by A54, A61, A63, ZFMISC_1:64; :: thesis:

end;

suppose A64: y in the carrier of CRtfsm2 ; :: thesis:

A65: y in Q' by A61, ZFMISC_1:64;
reconsider q = q as Element of Q by A7;
reconsider y = y as Element of Q by A65, ZFMISC_1:64;
( not q in the carrier of CRtfsm2 or not y in the carrier of CRtfsm2 or q = y ) by A1, Th79;
hence contradiction by A38, A64, A65, ZFMISC_1:64; :: thesis:

end;

hence contradiction by A55; :: thesis:

end;

suppose A66: x in the carrier of CRtfsm2 ; :: thesis:

reconsider q = q as Element of Q by A7;
reconsider x = x as Element of Q by A52, XBOOLE_0:def 5;
( not q in the carrier of CRtfsm2 or not x in the carrier of CRtfsm2 or q = x ) by A1, Th79;
hence contradiction by A38, A52, A66, ZFMISC_1:64; :: thesis:

end;

hence contradiction by A39; :: thesis:

end;