:: deftheorem defines -equivalent FSM_1:def 11 :
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm
for k being Nat holds
( k -equivalent qa,qb iff for w being FinSequence of IAlph st len w <= k holds
(qa,w) -response = (qb,w) -response );