:: deftheorem defines accessibleStates FSM_1:def 23 :
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph holds accessibleStates tfsm = { q where q is State of tfsm : q is accessible } ;