let x, z1, z2 be set ; :: thesis: for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega )
for TS being deterministic transition-system of F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
let E be non empty set ; :: thesis: for u, v being Element of E ^omega
for F being Subset of (E ^omega )
for TS being deterministic transition-system of F st u <> v & x,u -->. z1,TS & x,v -->. z2,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: for F being Subset of (E ^omega )
for TS being deterministic transition-system of F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
let F be Subset of (E ^omega ); :: thesis: for TS being deterministic transition-system of F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
let TS be deterministic transition-system of F; :: thesis: ( u <> v & x,u -->. z1,TS & x,v -->. z2,TS implies for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) )
assume that
A1: u <> v and
A2: ( x,u -->. z1,TS & x,v -->. z2,TS ) ; :: thesis: for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
x in TS by A2, ThProd30;
then reconsider x = x as Element of TS by STRUCT_0:def 5;
( [[x,u],z1] in the Tran of TS & [[x,v],z2] in the Tran of TS ) by A2, DefProd;
then ( [x,u] in dom the Tran of TS & [x,v] in dom the Tran of TS ) by RELAT_1:20;
hence for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) by A1, DefDetTS; :: thesis: verum