let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being transition-system over F st dom the Tran of TS = {} holds
TS is deterministic
let F be Subset of (E ^omega); :: thesis: for TS being transition-system over F st dom the Tran of TS = {} holds
TS is deterministic
let TS be transition-system over F; :: thesis: ( dom the Tran of TS = {} implies TS is deterministic )
assume dom the Tran of TS = {} ; :: thesis: TS is deterministic
then ( 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 ) ) ) ;
hence TS is deterministic ; :: thesis: verum