let it1, it2 be strict Mealy-FSM over IAlph,OAlph; ( the carrier of it1 = final_states_partition tfsm & ( for Q being State of it1
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . (q,s) in the Tran of it1 . (Q,s) & the OFun of tfsm . (q,s) = the OFun of it1 . (Q,s) ) ) & the InitS of tfsm in the InitS of it1 & the carrier of it2 = final_states_partition tfsm & ( for Q being State of it2
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . (q,s) in the Tran of it2 . (Q,s) & the OFun of tfsm . (q,s) = the OFun of it2 . (Q,s) ) ) & the InitS of tfsm in the InitS of it2 implies it1 = it2 )
set TR = the Tran of tfsm;
assume that
A12:
the carrier of it1 = final_states_partition tfsm
and
A13:
for Q being Element of it1
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . (q,s) in the Tran of it1 . (Q,s) & the OFun of tfsm . (q,s) = the OFun of it1 . (Q,s) )
and
A14:
the InitS of tfsm in the InitS of it1
; ( not the carrier of it2 = final_states_partition tfsm or ex Q being State of it2 ex s being Element of IAlph ex q being State of tfsm st
( q in Q & not ( the Tran of tfsm . (q,s) in the Tran of it2 . (Q,s) & the OFun of tfsm . (q,s) = the OFun of it2 . (Q,s) ) ) or not the InitS of tfsm in the InitS of it2 or it1 = it2 )
assume that
A15:
the carrier of it2 = final_states_partition tfsm
and
A16:
for Q being Element of it2
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . (q,s) in the Tran of it2 . (Q,s) & the OFun of tfsm . (q,s) = the OFun of it2 . (Q,s) )
and
A17:
the InitS of tfsm in the InitS of it2
; it1 = it2
A18:
the OFun of it1 = the OFun of it2
proof
reconsider OF2 = the
OFun of
it2 as
Function of
[:(final_states_partition tfsm),IAlph:],
OAlph by A15;
reconsider OF1 = the
OFun of
it1 as
Function of
[:(final_states_partition tfsm),IAlph:],
OAlph by A12;
now for Q being Element of final_states_partition tfsm
for s being Element of IAlph holds OF1 . (Q,s) = OF2 . (Q,s)let Q be
Element of
final_states_partition tfsm;
for s being Element of IAlph holds OF1 . (Q,s) = OF2 . (Q,s)let s be
Element of
IAlph;
OF1 . (Q,s) = OF2 . (Q,s)consider q being
Element of
tfsm such that A19:
q in Q
by FINSEQ_4:87;
thus OF1 . (
Q,
s) =
the
OFun of
tfsm . (
q,
s)
by A12, A13, A19
.=
OF2 . (
Q,
s)
by A15, A16, A19
;
verum end;
hence
the
OFun of
it1 = the
OFun of
it2
by BINOP_1:2;
verum
end;
A20:
the Tran of it1 = the Tran of it2
proof
reconsider T2 = the
Tran of
it2 as
Function of
[:(final_states_partition tfsm),IAlph:],
(final_states_partition tfsm) by A15;
reconsider T1 = the
Tran of
it1 as
Function of
[:(final_states_partition tfsm),IAlph:],
(final_states_partition tfsm) by A12;
now for Q being Element of final_states_partition tfsm
for s being Element of IAlph holds T1 . (Q,s) = T2 . (Q,s)let Q be
Element of
final_states_partition tfsm;
for s being Element of IAlph holds T1 . (Q,s) = T2 . (Q,s)let s be
Element of
IAlph;
T1 . (Q,s) = T2 . (Q,s)reconsider T19 =
T1 . [Q,s],
T29 =
T2 . [Q,s] as
Subset of
tfsm by TARSKI:def 3;
A21:
(
T19 = T29 or
T19 misses T29 )
by EQREL_1:def 4;
consider q being
Element of
tfsm such that A22:
q in Q
by FINSEQ_4:87;
( the
Tran of
tfsm . (
q,
s)
in T1 . (
Q,
s) & the
Tran of
tfsm . (
q,
s)
in T2 . (
Q,
s) )
by A12, A13, A15, A16, A22;
hence
T1 . (
Q,
s)
= T2 . (
Q,
s)
by A21, XBOOLE_0:3;
verum end;
hence
the
Tran of
it1 = the
Tran of
it2
by BINOP_1:2;
verum
end;
the InitS of it1 = the InitS of it2
hence
it1 = it2
by A12, A15, A20, A18; verum