let IAlph, OAlph be non empty set ; for Rtfsm being non empty finite reduced Mealy-FSM over IAlph,OAlph holds Rtfsm, the_reduction_of Rtfsm -are_isomorphic
let Rtfsm be non empty finite reduced Mealy-FSM over IAlph,OAlph; Rtfsm, the_reduction_of Rtfsm -are_isomorphic
set m = Rtfsm;
set rm = the_reduction_of Rtfsm;
set fpm = final_states_partition Rtfsm;
deffunc H1( Element of Rtfsm) -> Element of final_states_partition Rtfsm = (proj (final_states_partition Rtfsm)) . $1;
consider Tf being Function of the carrier of Rtfsm,(final_states_partition Rtfsm) such that
A1:
for q being Element of Rtfsm holds Tf . q = H1(q)
from FUNCT_2:sch 4();
set Im1 = the InitS of Rtfsm;
A9:
final_states_partition Rtfsm c= rng Tf
rng Tf c= final_states_partition Rtfsm
by RELAT_1:def 19;
then
rng Tf = final_states_partition Rtfsm
by A9;
then A12:
Tf is onto
by FUNCT_2:def 3;
A13:
the carrier of (the_reduction_of Rtfsm) = final_states_partition Rtfsm
by Def18;
A14:
now for q being State of Rtfsm
for s being Element of IAlph holds
( Tf . ( the Tran of Rtfsm . (q,s)) = the Tran of (the_reduction_of Rtfsm) . ((Tf . q),s) & the OFun of Rtfsm . (q,s) = the OFun of (the_reduction_of Rtfsm) . ((Tf . q),s) )let q be
State of
Rtfsm;
for s being Element of IAlph holds
( Tf . ( the Tran of Rtfsm . (q,s)) = the Tran of (the_reduction_of Rtfsm) . ((Tf . q),s) & the OFun of Rtfsm . (q,s) = the OFun of (the_reduction_of Rtfsm) . ((Tf . q),s) )let s be
Element of
IAlph;
( Tf . ( the Tran of Rtfsm . (q,s)) = the Tran of (the_reduction_of Rtfsm) . ((Tf . q),s) & the OFun of Rtfsm . (q,s) = the OFun of (the_reduction_of Rtfsm) . ((Tf . q),s) )reconsider Tfq =
Tf . q as
State of
(the_reduction_of Rtfsm) by Def18;
A15:
the
Tran of
(the_reduction_of Rtfsm) . [Tfq,s] is
State of
(the_reduction_of Rtfsm)
;
Tf . q = (proj (final_states_partition Rtfsm)) . q
by A1;
then A16:
q in Tf . q
by EQREL_1:def 9;
then
the
Tran of
Rtfsm . (
q,
s)
in the
Tran of
(the_reduction_of Rtfsm) . (
(Tf . q),
s)
by A13, Def18;
then
the
Tran of
(the_reduction_of Rtfsm) . [(Tf . q),s] = (proj (final_states_partition Rtfsm)) . ( the Tran of Rtfsm . [q,s])
by A13, A15, EQREL_1:65;
hence
Tf . ( the Tran of Rtfsm . (q,s)) = the
Tran of
(the_reduction_of Rtfsm) . (
(Tf . q),
s)
by A1;
the OFun of Rtfsm . (q,s) = the OFun of (the_reduction_of Rtfsm) . ((Tf . q),s)thus
the
OFun of
Rtfsm . (
q,
s)
= the
OFun of
(the_reduction_of Rtfsm) . (
(Tf . q),
s)
by A13, A16, Def18;
verum end;
the InitS of Rtfsm in the InitS of (the_reduction_of Rtfsm)
by Def18;
then
the InitS of (the_reduction_of Rtfsm) = (proj (final_states_partition Rtfsm)) . the InitS of Rtfsm
by A13, EQREL_1:65;
then
Tf . the InitS of Rtfsm = the InitS of (the_reduction_of Rtfsm)
by A1;
hence
Rtfsm, the_reduction_of Rtfsm -are_isomorphic
by A13, A2, A12, A14; verum