let x, y1, y2, z be object ; :: thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
let TS be non empty transition-system over F; :: thesis: ( TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] implies y1 = y2 )
assume A1: TS is deterministic ; :: thesis: ( not ==>.-relation TS reduces x,[y1,z] or not ==>.-relation TS reduces x,[y2,z] or y1 = y2 )
assume that
A2: ==>.-relation TS reduces x,[y1,z] and
A3: ==>.-relation TS reduces x,[y2,z] ; :: thesis: y1 = y2
consider P being RedSequence of ==>.-relation TS such that
A4: P . 1 = x and
A5: P . (len P) = [y1,z] by A2, REWRITE1:def 3;
consider Q being RedSequence of ==>.-relation TS such that
A6: Q . 1 = x and
A7: Q . (len Q) = [y2,z] by A3, REWRITE1:def 3;
A8: (Q . (len Q)) `2 = z by A7;
(P . (len P)) `2 = z by A5;
then P = Q by A1, A4, A6, A8, Th69;
hence y1 = y2 by A5, A7, XTUPLE_0:1; :: thesis: verum