:: deftheorem defines -leads_to FSM_1:def 3 :
for IAlph being non empty set
for fsm being non empty FSM over IAlph
for w being FinSequence of IAlph
for q1, q2 being State of fsm holds
( q1,w -leads_to q2 iff ((q1,w) -admissible) . ((len w) + 1) = q2 );