:: deftheorem Def2 defines -admissible FSM_1:def 2 :
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for q being State of fsm
for w being FinSequence of IAlph
for b₅ being FinSequence of the carrier of fsm holds
( b₅ = (q,w) -admissible iff ( b₅ . 1 = q & len b₅ = (len w) + 1 & ( for i being Nat st 1 <= i & i <= len w holds
ex wi being Element of IAlph ex qi, qi1 being State of fsm st
( wi = w . i & qi = b₅ . i & qi1 = b₅ . (i + 1) & wi -succ_of qi = qi1 ) ) ) );