let E be non empty set ; :: thesis: 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; :: thesis: ( the Tran of TS is Function implies TS is deterministic )

assume A1: the Tran of TS is Function ; :: thesis: TS is deterministic

hence TS is deterministic by A1, A2, REWRITE3:def 1; :: thesis: verum

TS is deterministic

let TS be transition-system over Lex E; :: thesis: ( the Tran of TS is Function implies TS is deterministic )

assume A1: the Tran of TS is Function ; :: thesis: TS is deterministic

A2: now :: thesis: 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 )

not <%> E in rng (dom the Tran of TS)
by Th8;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; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum

end;for w being Element of E ^omega holds

( not u ^ w = v & not v ^ w = u )

let u, v be Element of E ^omega ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum

hence TS is deterministic by A1, A2, REWRITE3:def 1; :: thesis: verum