let x, z1, z2 be object ; :: 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 over 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 over 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 over 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 over 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 over 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 and
A3: 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, Th15;
then reconsider x = x as Element of TS ;
[[x,v],z2] in the Tran of TS by A3;
then A4: [x,v] in dom the Tran of TS by XTUPLE_0:def 12;
[[x,u],z1] in the Tran of TS by A2;
then [x,u] in dom the Tran of TS by XTUPLE_0:def 12;
hence for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) by A1, A4, Def1; :: thesis: verum