let IAlph, OAlph be non empty set ; :: thesis:
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis:
let CRtfsm1, CRtfsm2 be non empty finite reduced connected Mealy-FSM over IAlph,OAlph; :: thesis:
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
assume that
A1: the carrier of CRtfsm1 misses the carrier of CRtfsm2 and
A2: CRtfsm1,CRtfsm2 -are_equivalent and
A3: tfsm = CRtfsm1 -Mealy_union CRtfsm2 ; :: thesis:
set ISrtfsm2 = the InitS of CRtfsm2;
set ISrtfsm1 = the InitS of CRtfsm1;
A4: the carrier of CRtfsm1 /\ the carrier of CRtfsm2 = {} by A1;
set Stfsm = the carrier of tfsm;
set Srtfsm2 = the carrier of CRtfsm2;
set Srtfsm1 = the carrier of CRtfsm1;
set rtfsm = the_reduction_of tfsm;
set Srtfsm = the carrier of (the_reduction_of tfsm);
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
A5: 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 ) ) ;
A6: 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;
union (final_states_partition tfsm) = the carrier of tfsm by EQREL_1:def 4
.= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A3, Def24 ;
then A7: Q c= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A6, ZFMISC_1:74;
Q in the carrier of (the_reduction_of tfsm) ;
then A8: Q in final_states_partition tfsm by Def18;
then A9: Q <> {} ;
then consider q being Element of the carrier of tfsm such that
A10: q in Q by SUBSET_1:4;

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

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

set Q9 = Q \ {q};

A12: now :: thesis:

A13: Q \ {q} c= Q by XBOOLE_1:36;
reconsider Q = Q as Subset of the carrier of tfsm ;
assume A14: Q \ {q} <> {} ; :: thesis:
reconsider Q9 = Q \ {q} as Subset of the carrier of tfsm ;
consider x being Element of the carrier of tfsm such that
A15: x in Q9 by A14, SUBSET_1:4;
A16: Q9 c= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A7, A13;

per cases by A15, A16, XBOOLE_0:def 3;

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

reconsider x = x as Element of Q by A15, XBOOLE_0:def 5;
reconsider q = q as Element of Q by A10;
( not q in the carrier of CRtfsm1 or not x in the carrier of CRtfsm1 or q = x ) by A1, A3, Th59;
hence contradiction by A11, A15, A17, ZFMISC_1:56; :: thesis:

end;

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

set Q99 = Q9 \ {x};

A19: now :: thesis:

A20: Q9 \ {x} c= Q9 by XBOOLE_1:36;
reconsider Q9 = Q9 as Subset of the carrier of tfsm ;
assume A21: Q9 \ {x} <> {} ; :: thesis:
reconsider Q99 = Q9 \ {x} as Subset of the carrier of tfsm ;
consider y being Element of the carrier of tfsm such that
A22: y in Q99 by A21, SUBSET_1:4;
A23: Q99 c= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A16, A20;

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

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

reconsider q = q as Element of Q by A10;
A25: y in Q9 by A22, ZFMISC_1:56;
then reconsider y = y as Element of Q by ZFMISC_1:56;
( not q in the carrier of CRtfsm1 or not y in the carrier of CRtfsm1 or q = y ) by A1, A3, Th59;
hence contradiction by A11, A24, A25, ZFMISC_1:56; :: thesis:

end;

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

reconsider x = x as Element of Q by A15, ZFMISC_1:56;
y in Q9 by A22, ZFMISC_1:56;
then reconsider y = y as Element of Q by ZFMISC_1:56;
( not x in the carrier of CRtfsm2 or not y in the carrier of CRtfsm2 or x = y ) by A3, Th60;
hence contradiction by A18, A22, A26, ZFMISC_1:56; :: thesis:

end;

now :: thesis:

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

proof

given z being Element of Q such that A29: z <> q and
A30: z <> x ; :: thesis:
z in Q9 by A9, A29, ZFMISC_1:56;
hence contradiction by A27, A30, ZFMISC_1:56; :: thesis:

end;

reconsider x = x as Element of Q by A15, ZFMISC_1:56;
reconsider q = q as Element of Q by A10;
( 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 A5;
hence contradiction by A11, A18, A28; :: thesis:

end;

hence contradiction by A19; :: thesis:

end;

now :: thesis:

reconsider q = q as Element of the carrier of CRtfsm1 by A11;
q is accessible by Def22;
then consider w being FinSequence of IAlph such that
A31: the InitS of CRtfsm1,w -leads_to q ;
set adl = the InitS of CRtfsm2 leads_to_under w;

A32: now :: thesis:

reconsider q = q as Element of the carrier of tfsm ;
assume A33: not the InitS of CRtfsm2 leads_to_under w in Q ; :: thesis:
reconsider q1 = q as Element of the carrier of CRtfsm1 ;
the InitS of CRtfsm2 leads_to_under w in the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by XBOOLE_0:def 3;
then reconsider adl = the InitS of CRtfsm2 leads_to_under w as Element of the carrier of tfsm by A3, Def24;
A34: for Y being Element of the carrier of (the_reduction_of tfsm) holds
( not q in Y or not adl in Y )

proof

reconsider Q = Q as Subset of the carrier of tfsm ;
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
A35: q in Y and
A36: adl in Y ;
reconsider Y = Y as Subset of the carrier of tfsm by A6, 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 A8, A33, A36, EQREL_1:def 4;
hence contradiction by A10, A35, XBOOLE_0:3; :: thesis:

end;

reconsider adl2 = adl as Element of the carrier of CRtfsm2 ;
final_states_partition tfsm is final by Def15;
then not q,adl -are_equivalent by A6, A34;
then consider dseq being FinSequence of IAlph such that
A37: (q,dseq) -response <> (adl,dseq) -response ;
(q,dseq) -response = (q1,dseq) -response by A1, A3, Th53;
then A38: (q1,dseq) -response <> (adl2,dseq) -response by A3, A37, Th55;
the InitS of CRtfsm2,w -leads_to adl2 by Def5;
then ( the InitS of CRtfsm1,(w ^ dseq)) -response <> ( the InitS of CRtfsm2,(w ^ dseq)) -response by A31, A38, Th12;
hence contradiction by A2; :: thesis:

end;

assume A39: Q \ {q} = {} ; :: thesis:

now :: thesis:

assume A40: the InitS of CRtfsm2 leads_to_under w in Q ; :: thesis:
the InitS of CRtfsm2 leads_to_under w <> q by A4, XBOOLE_0:def 4;
hence contradiction by A39, A40, ZFMISC_1:56; :: thesis:

end;

hence contradiction by A32; :: thesis:

end;

hence contradiction by A12; :: thesis:

end;

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

set Q9 = Q \ {q};

A42: now :: thesis:

A43: Q \ {q} c= Q by XBOOLE_1:36;
reconsider Q = Q as Subset of the carrier of tfsm ;
assume A44: Q \ {q} <> {} ; :: thesis:
reconsider Q9 = Q \ {q} as Subset of the carrier of tfsm ;
consider x being Element of the carrier of tfsm such that
A45: x in Q9 by A44, SUBSET_1:4;
A46: Q9 c= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A7, A43;

per cases by A45, A46, XBOOLE_0:def 3;

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

set Q99 = Q9 \ {x};

A48: now :: thesis:

A49: Q9 \ {x} c= Q9 by XBOOLE_1:36;
reconsider Q9 = Q9 as Subset of the carrier of tfsm ;
assume A50: Q9 \ {x} <> {} ; :: thesis:
reconsider Q99 = Q9 \ {x} as Subset of the carrier of tfsm ;
consider y being Element of the carrier of tfsm such that
A51: y in Q99 by A50, SUBSET_1:4;
A52: Q99 c= the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A46, A49;

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

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

reconsider x = x as Element of Q by A45, ZFMISC_1:56;
y in Q9 by A51, ZFMISC_1:56;
then reconsider y = y as Element of Q by ZFMISC_1:56;
( not x in the carrier of CRtfsm1 or not y in the carrier of CRtfsm1 or x = y ) by A1, A3, Th59;
hence contradiction by A47, A51, A53, ZFMISC_1:56; :: thesis:

end;

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

reconsider q = q as Element of Q by A10;
A55: y in Q9 by A51, ZFMISC_1:56;
then reconsider y = y as Element of Q by ZFMISC_1:56;
( not q in the carrier of CRtfsm2 or not y in the carrier of CRtfsm2 or q = y ) by A3, Th60;
hence contradiction by A41, A54, A55, ZFMISC_1:56; :: thesis:

end;

now :: thesis:

assume A56: Q9 \ {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 and
A59: z <> x ; :: thesis:
z in Q9 by A9, A58, ZFMISC_1:56;
hence contradiction by A56, A59, ZFMISC_1:56; :: thesis:

end;

reconsider x = x as Element of Q by A45, ZFMISC_1:56;
reconsider q = q as Element of Q by A10;
( 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 A5;
hence contradiction by A41, A47, A57; :: thesis:

end;

hence contradiction by A48; :: thesis:

end;

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

reconsider x = x as Element of Q by A45, XBOOLE_0:def 5;
reconsider q = q as Element of Q by A10;
( not q in the carrier of CRtfsm2 or not x in the carrier of CRtfsm2 or q = x ) by A3, Th60;
hence contradiction by A41, A45, A60, ZFMISC_1:56; :: thesis:

end;

now :: thesis:

reconsider q = q as Element of the carrier of CRtfsm2 by A41;
q is accessible by Def22;
then consider w being FinSequence of IAlph such that
A61: the InitS of CRtfsm2,w -leads_to q ;
set adl = the InitS of CRtfsm1 leads_to_under w;

A62: now :: thesis:

reconsider q = q as Element of the carrier of tfsm ;
assume A63: not the InitS of CRtfsm1 leads_to_under w in Q ; :: thesis:
reconsider q1 = q as Element of the carrier of CRtfsm2 ;
the InitS of CRtfsm1 leads_to_under w in the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by XBOOLE_0:def 3;
then reconsider adl = the InitS of CRtfsm1 leads_to_under w as Element of the carrier of tfsm by A3, Def24;
A64: 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
A65: q in Y and
A66: adl in Y ;
reconsider Y = Y as Subset of the carrier of tfsm by A6, 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 A8, A63, A66, EQREL_1:def 4;
hence contradiction by A10, A65, XBOOLE_0:3; :: thesis:

end;

reconsider adl2 = adl as Element of the carrier of CRtfsm1 ;
final_states_partition tfsm is final by Def15;
then not q,adl -are_equivalent by A6, A64;
then consider dseq being FinSequence of IAlph such that
A67: (q,dseq) -response <> (adl,dseq) -response ;
(q,dseq) -response = (q1,dseq) -response by A3, Th55;
then A68: (q1,dseq) -response <> (adl2,dseq) -response by A1, A3, A67, Th53;
the InitS of CRtfsm1,w -leads_to adl2 by Def5;
then ( the InitS of CRtfsm2,(w ^ dseq)) -response <> ( the InitS of CRtfsm1,(w ^ dseq)) -response by A61, A68, Th12;
hence contradiction by A2; :: thesis:

end;

assume A69: Q \ {q} = {} ; :: thesis:

now :: thesis:

assume A70: 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 A69, A70, ZFMISC_1:56; :: thesis:

end;

hence contradiction by A62; :: thesis:

end;

hence contradiction by A42; :: thesis:

end;