:: deftheorem defines accessible FSM_1:def 21 :
for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for IT being State of tfsm holds
( IT is accessible iff ex w being FinSequence of IAlph st the InitS of tfsm,w -leads_to IT );