let x1, x2, y1, y2, z1, z2 be object ; :: thesis: for E being non empty set
for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds
( y1 = y2 & z1 = z2 )
let E be non empty set ; :: thesis: for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds
( y1 = y2 & z1 = z2 )
let F be Subset of (E ^omega); :: thesis: for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds
( y1 = y2 & z1 = z2 )
let TS be deterministic transition-system over F; :: thesis: ( x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS implies ( y1 = y2 & z1 = z2 ) )
assume that
A1: x1,x2 ==>. y1,z1,TS and
A2: x1,x2 ==>. y2,z2,TS ; :: thesis: ( y1 = y2 & z1 = z2 )
consider v2, w2 being Element of E ^omega such that
A3: v2 = z2 and
A4: x1,w2 -->. y2,TS and
A5: x2 = w2 ^ v2 by A2;
consider v1, w1 being Element of E ^omega such that
A6: v1 = z1 and
A7: x1,w1 -->. y1,TS and
A8: x2 = w1 ^ v1 by A1;
A9: the Tran of TS is Function by Def1;
( ex u9 being Element of E ^omega st
( w1 ^ u9 = w2 & v1 = u9 ^ v2 ) or ex u9 being Element of E ^omega st
( w2 ^ u9 = w1 & v2 = u9 ^ v1 ) ) by A8, A5, Th13;
then w1 = w2 by A7, A4, Th19;
then v1 = v2 by A8, A5, AFINSQ_1:28;
hence ( y1 = y2 & z1 = z2 ) by A1, A2, A6, A3, A9, Th27; :: thesis: verum