:: deftheorem Def6 defines halting FSM_2:def 6 :
for I being non empty set
for S being non empty SM_Final over I holds
( S is halting iff for s being Element of I holds s leads_to_final_state_of S );