let IAlph, OAlph be non empty set ; for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for Rtfsm1, Rtfsm2 being non empty reduced Mealy-FSM over IAlph,OAlph st tfsm = Rtfsm1 -Mealy_union Rtfsm2 & the carrier of Rtfsm1 misses the carrier of Rtfsm2 & Rtfsm1,Rtfsm2 -are_equivalent holds
ex Q being State of (the_reduction_of tfsm) st
( the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q & Q = the InitS of (the_reduction_of tfsm) )
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; for Rtfsm1, Rtfsm2 being non empty reduced Mealy-FSM over IAlph,OAlph st tfsm = Rtfsm1 -Mealy_union Rtfsm2 & the carrier of Rtfsm1 misses the carrier of Rtfsm2 & Rtfsm1,Rtfsm2 -are_equivalent holds
ex Q being State of (the_reduction_of tfsm) st
( the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q & Q = the InitS of (the_reduction_of tfsm) )
let Rtfsm1, Rtfsm2 be non empty reduced Mealy-FSM over IAlph,OAlph; ( tfsm = Rtfsm1 -Mealy_union Rtfsm2 & the carrier of Rtfsm1 misses the carrier of Rtfsm2 & Rtfsm1,Rtfsm2 -are_equivalent implies ex Q being State of (the_reduction_of tfsm) st
( the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q & Q = the InitS of (the_reduction_of tfsm) ) )
set rtfsm1 = Rtfsm1;
set rtfsm2 = Rtfsm2;
assume that
A1:
tfsm = Rtfsm1 -Mealy_union Rtfsm2
and
A2:
the carrier of Rtfsm1 misses the carrier of Rtfsm2
and
A3:
Rtfsm1,Rtfsm2 -are_equivalent
; ex Q being State of (the_reduction_of tfsm) st
( the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q & Q = the InitS of (the_reduction_of tfsm) )
set Srtfsm2 = the carrier of Rtfsm2;
set Stfsm = the carrier of tfsm;
set Srtfsm1 = the carrier of Rtfsm1;
the carrier of tfsm = the carrier of Rtfsm1 \/ the carrier of Rtfsm2
by A1, Def24;
then reconsider IS2 = the InitS of Rtfsm2 as Element of the carrier of tfsm by XBOOLE_0:def 3;
reconsider IS1 = the InitS of Rtfsm1 as Element of the carrier of tfsm by A1, Def24;
now for w being FinSequence of IAlph holds (IS1,w) -response = (IS2,w) -response let w be
FinSequence of
IAlph;
(IS1,w) -response = (IS2,w) -response
( the
InitS of
Rtfsm1,
w)
-response = ( the
InitS of
Rtfsm2,
w)
-response
by A3;
hence (
IS1,
w)
-response =
( the
InitS of
Rtfsm2,
w)
-response
by A1, A2, Th53
.=
(
IS2,
w)
-response
by A1, Th55
;
verum end;
then A4:
IS1,IS2 -are_equivalent
;
set RUN = the_reduction_of tfsm;
the InitS of tfsm = the InitS of Rtfsm1
by A1, Def24;
then A5:
the InitS of Rtfsm1 in the InitS of (the_reduction_of tfsm)
by Def18;
set SRUN = the carrier of (the_reduction_of tfsm);
A6:
the carrier of (the_reduction_of tfsm) = final_states_partition tfsm
by Def18;
final_states_partition tfsm is final
by Def15;
then consider X being Element of the carrier of (the_reduction_of tfsm) such that
A7:
IS1 in X
and
A8:
IS2 in X
by A6, A4;
take
X
; ( the InitS of Rtfsm1 in X & the InitS of Rtfsm2 in X & X = the InitS of (the_reduction_of tfsm) )
thus
( the InitS of Rtfsm1 in X & the InitS of Rtfsm2 in X )
by A7, A8; X = the InitS of (the_reduction_of tfsm)
( X is Subset of the carrier of tfsm & the InitS of (the_reduction_of tfsm) is Subset of the carrier of tfsm )
by A6, TARSKI:def 3;
then
( X = the InitS of (the_reduction_of tfsm) or X misses the InitS of (the_reduction_of tfsm) )
by A6, EQREL_1:def 4;
hence
X = the InitS of (the_reduction_of tfsm)
by A7, A5, XBOOLE_0:3; verum