:: deftheorem Def20 defines reduced FSM_1:def 20 :
for IAlph, OAlph being non empty set
for IT being non empty Mealy-FSM over IAlph,OAlph holds
( IT is reduced iff for qa, qb being State of IT st qa <> qb holds
not qa,qb -are_equivalent );