let E be non empty set ; for TS being transition-system over Lex E st the Tran of TS is Function holds
TS is deterministic
let TS be transition-system over Lex E; ( the Tran of TS is Function implies TS is deterministic )
assume A1:
the Tran of TS is Function
; TS is deterministic
A2:
now for p being Element of TS
for u, v being Element of E ^omega st u <> v & [p,u] in dom the Tran of TS & [p,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )let p be
Element of
TS;
for u, v being Element of E ^omega st u <> v & [p,u] in dom the Tran of TS & [p,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )let u,
v be
Element of
E ^omega ;
( u <> v & [p,u] in dom the Tran of TS & [p,v] in dom the Tran of TS implies for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) )assume that A3:
u <> v
and A4:
(
[p,u] in dom the
Tran of
TS &
[p,v] in dom the
Tran of
TS )
;
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
(
u in Lex E &
v in Lex E )
by A4, ZFMISC_1:87;
hence
for
w being
Element of
E ^omega holds
( not
u ^ w = v & not
v ^ w = u )
by A3, Th10;
verum end;
not <%> E in rng (dom the Tran of TS)
by Th8;
hence
TS is deterministic
by A1, A2, REWRITE3:def 1; verum