:: deftheorem Def7 defines -TwoStatesMooreSM FSM_2:def 7 :
for I, O being non empty set
for i, f being set
for o being Function of {i,f},O
for b₆ being non empty strict Moore-SM_Final over I,O holds
( b₆ = I -TwoStatesMooreSM (i,f,o) iff ( the carrier of b₆ = {i,f} & the Tran of b₆ = [:{i,f},I:] --> f & the OFun of b₆ = o & the InitS of b₆ = i & the FinalS of b₆ = {f} ) );