:: deftheorem defines is_result_of FSM_2:def 8 :
for I, O being non empty set
for M being non empty Moore-SM_Final over I,O
for s being Element of I
for t being object holds
( t is_result_of s,M iff ex m being non zero Element of NAT st
for w being FinSequence of I st w . 1 = s holds
( ( m <= (len w) + 1 implies ( t = the OFun of M . ((GEN (w, the InitS of M)) . m) & (GEN (w, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds
not (GEN (w, the InitS of M)) . n in the FinalS of M ) ) );