:: deftheorem Def1 defines _bool FSM_3:def 1 :
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for b₄ being strict transition-system over Lex E holds
( b₄ = _bool TS iff ( the carrier of b₄ = bool the carrier of TS & ( for S being Subset of TS
for w being Element of E ^omega
for T being Subset of TS holds
( [[S,w],T] in the Tran of b₄ iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) ) );