:: deftheorem Def1 defines deterministic REWRITE3:def 1 :
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( TS is deterministic iff ( the Tran of TS is Function & not <%> E in rng (dom the Tran of TS) & ( for s being Element of TS
for u, v being Element of E ^omega st u <> v & [s,u] in dom the Tran of TS & [s,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) ) ) );