let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm = CRtfsm1 -Mealy_union CRtfsm2 holds
for Q being State of (the_reduction_of tfsm)
for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm1 or not q2 in the carrier of CRtfsm1 or not q1 <> q2 )
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm = CRtfsm1 -Mealy_union CRtfsm2 holds
for Q being State of (the_reduction_of tfsm)
for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm1 or not q2 in the carrier of CRtfsm1 or not q1 <> q2 )
let CRtfsm1, CRtfsm2 be non empty finite reduced connected Mealy-FSM over IAlph,OAlph; :: thesis: ( the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm = CRtfsm1 -Mealy_union CRtfsm2 implies for Q being State of (the_reduction_of tfsm)
for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm1 or not q2 in the carrier of CRtfsm1 or not q1 <> q2 ) )
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
assume that
A1: the carrier of CRtfsm1 misses the carrier of CRtfsm2 and
A2: tfsm = CRtfsm1 -Mealy_union CRtfsm2 ; :: thesis: for Q being State of (the_reduction_of tfsm)
for q1, q2 being Element of Q holds
( not q1 in the carrier of CRtfsm1 or not q2 in the carrier of CRtfsm1 or not q1 <> q2 )
given Q being Element of (the_reduction_of tfsm), q1, q2 being Element of Q such that A3: ( q1 in the carrier of CRtfsm1 & q2 in the carrier of CRtfsm1 ) and
A4: q1 <> q2 ; :: thesis: contradiction
consider tfsm1 being non empty finite Mealy-FSM over IAlph,OAlph such that
A5: CRtfsm1, the_reduction_of tfsm1 -are_isomorphic by Th47;
set tfsm1r = the_reduction_of tfsm1;
consider Tf being Function of the carrier of CRtfsm1, the carrier of (the_reduction_of tfsm1) such that
A6: Tf is bijective and
Tf . the InitS of CRtfsm1 = the InitS of (the_reduction_of tfsm1) and
A7: for q being State of CRtfsm1
for s being Element of IAlph holds
( Tf . ( the Tran of CRtfsm1 . (q,s)) = the Tran of (the_reduction_of tfsm1) . ((Tf . q),s) & the OFun of CRtfsm1 . (q,s) = the OFun of (the_reduction_of tfsm1) . ((Tf . q),s) ) by A5;
A8: dom Tf = the carrier of CRtfsm1 by FUNCT_2:def 1;
then A9: Tf . q1 <> Tf . q2 by A3, A4, A6, FUNCT_1:def 4;
rng Tf = the carrier of (the_reduction_of tfsm1) by A6, FUNCT_2:def 3;
then reconsider Tq1 = Tf . q1, Tq2 = Tf . q2 as Element of (the_reduction_of tfsm1) by A3, A8, FUNCT_1:def 3;
the carrier of tfsm = the carrier of CRtfsm1 \/ the carrier of CRtfsm2 by A2, Def24;
then reconsider q1 = q1, q2 = q2 as Element of tfsm by A3, XBOOLE_0:def 3;
reconsider q19 = q1, q29 = q2 as Element of CRtfsm1 by A3;
not Tq1,Tq2 -are_equivalent by A9, Th45;
then A10: not q19,q29 -are_equivalent by A7, Th44;
set rtfsm = the_reduction_of tfsm;
A11: final_states_partition tfsm is final by Def15;
A12: the carrier of (the_reduction_of tfsm) = final_states_partition tfsm by Def18;
then reconsider Q = Q as Subset of tfsm by TARSKI:def 3;
q1,q2 -are_equivalent by A11, A12;
hence contradiction by A1, A2, A10, Th57; :: thesis: verum