let x, y1, y2, z be object ; 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 ; 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); 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; ( TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] implies y1 = y2 )
assume A1:
TS is deterministic
; ( 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]
; 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; verum