let x, y, 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 holds
( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
let E be non empty set ; for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
let F be Subset of (E ^omega); for TS being non empty transition-system over F holds
( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
let TS be non empty transition-system over F; ( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
thus
( x,y -->. z,TS implies <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
( <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS implies x,y -->. z,TS )proof
assume
x,
y -->. z,
TS
;
<*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS
then
[[x,y],[z,(<%> E)]] in ==>.-relation TS
by Th37;
hence
<*[x,y],[z,(<%> E)]*> is
RedSequence of
==>.-relation TS
by REWRITE1:7;
verum
end;
assume
<*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS
; x,y -->. z,TS
then
[[x,y],[z,(<%> E)]] in ==>.-relation TS
by Th8;
hence
x,y -->. z,TS
by Th37; verum