:: deftheorem Def6 defines -response FSM_1:def 6 :
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qt being State of tfsm
for w being FinSequence of IAlph
for b₆ being FinSequence of OAlph holds
( b₆ = (qt,w) -response iff ( len b₆ = len w & ( for i being Nat st i in dom w holds
b₆ . i = the OFun of tfsm . [(((qt,w) -admissible) . i),(w . i)] ) ) );