:: deftheorem defines calculating_type FSM_2:def 1 :
for I being non empty set
for S being non empty FSM over I holds
( S is calculating_type iff for j being non zero Element of NAT
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds
(GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j );