let x1, x2, y1, z, y2 be set ; :: thesis: for E being non empty set
for F being Subset of (E ^omega )
for TS being non empty transition-system of F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds
y1 = y2
let E be non empty set ; :: thesis: for F being Subset of (E ^omega )
for TS being non empty transition-system of F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds
y1 = y2
let F be Subset of (E ^omega ); :: thesis: for TS being non empty transition-system of F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds
y1 = y2
let TS be non empty transition-system of F; :: thesis: ( TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS implies y1 = y2 )
assume A: TS is deterministic ; :: thesis: ( not x1,x2 ==>* y1,z,TS or not x1,x2 ==>* y2,z,TS or y1 = y2 )
assume that
B1: x1,x2 ==>* y1,z,TS and
B2: x1,x2 ==>* y2,z,TS ; :: thesis: y1 = y2
C1: ==>.-relation TS reduces [x1,x2],[y1,z] by B1, DefTran;
C2: ==>.-relation TS reduces [x1,x2],[y2,z] by B2, DefTran;
thus y1 = y2 by A, C1, C2, ThRed140; :: thesis: verum