theorem
for
IAlph,
OAlph being non
empty set for
tfsm being non
empty finite Mealy-FSM over
IAlph,
OAlph for
cTran being
Function of
[:(accessibleStates tfsm),IAlph:],
(accessibleStates tfsm) for
cOFun being
Function of
[:(accessibleStates tfsm),IAlph:],
OAlph for
cInitS being
Element of
accessibleStates tfsm st
cTran = the
Tran of
tfsm | [:(accessibleStates tfsm),IAlph:] &
cOFun = the
OFun of
tfsm | [:(accessibleStates tfsm),IAlph:] &
cInitS = the
InitS of
tfsm holds
tfsm,
Mealy-FSM(#
(accessibleStates tfsm),
cTran,
cOFun,
cInitS #)
-are_equivalent