:: deftheorem Def18 defines the_reduction_of FSM_1:def 18 :
for IAlph, OAlph being non empty set
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for b₄ being strict Mealy-FSM over IAlph,OAlph holds
( b₄ = the_reduction_of tfsm iff ( the carrier of b₄ = final_states_partition tfsm & ( for Q being State of b₄
for s being Element of IAlph
for q being State of tfsm st q in Q holds
( the Tran of tfsm . (q,s) in the Tran of b₄ . (Q,s) & the OFun of tfsm . (q,s) = the OFun of b₄ . (Q,s) ) ) & the InitS of tfsm in the InitS of b₄ ) );