:: deftheorem Def12 defines -eq_states_EqR FSM_1:def 12 :
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for i being Nat
for b₅ being Equivalence_Relation of the carrier of tfsm holds
( b₅ = i -eq_states_EqR tfsm iff for qa, qb being State of tfsm holds
( [qa,qb] in b₅ iff i -equivalent qa,qb ) );