:: deftheorem Def7 defines -response FSM_1:def 7 :
for IAlph, OAlph being non empty set
for sfsm being non empty Moore-FSM over IAlph,OAlph
for qs being State of sfsm
for w being FinSequence of IAlph
for b₆ being FinSequence of OAlph holds
( b₆ = (qs,w) -response iff ( len b₆ = (len w) + 1 & ( for i being Nat st i in Seg ((len w) + 1) holds
b₆ . i = the OFun of sfsm . (((qs,w) -admissible) . i) ) ) );