let X be set ; :: thesis: for E being non empty set

for w being Element of E ^omega

for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let E be non empty set ; :: thesis: for w being Element of E ^omega

for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let w be Element of E ^omega ; :: thesis: for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F

for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let TS be non empty transition-system over F; :: thesis: for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let S be Subset of TS; :: thesis: ( len w = 1 implies ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) )

assume A1: len w = 1 ; :: thesis: ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

thus ( X = w -succ_of (S,TS) implies S,w ==>* X, _bool TS ) :: thesis: ( S,w ==>* X, _bool TS implies X = w -succ_of (S,TS) )

then A2: S,w ==>* X, <%> E, _bool TS by REWRITE3:def 7;

ex e being Element of E st

( w = <%e%> & w . 0 = e ) by A1, Th4;

then S,w ^ {} ==>. X, <%> E, _bool TS by A2, Th12;

then A3: S,w -->. X, _bool TS by REWRITE3:24;

then X in _bool TS by REWRITE3:15;

then X in the carrier of (_bool TS) ;

then reconsider X9 = X as Subset of TS by Def1;

[[S,w],X9] in the Tran of (_bool TS) by A3, REWRITE3:def 2;

hence X = w -succ_of (S,TS) by Def1; :: thesis: verum

for w being Element of E ^omega

for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let E be non empty set ; :: thesis: for w being Element of E ^omega

for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let w be Element of E ^omega ; :: thesis: for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let F be Subset of (E ^omega); :: thesis: for TS being non empty transition-system over F

for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let TS be non empty transition-system over F; :: thesis: for S being Subset of TS st len w = 1 holds

( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

let S be Subset of TS; :: thesis: ( len w = 1 implies ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS ) )

assume A1: len w = 1 ; :: thesis: ( X = w -succ_of (S,TS) iff S,w ==>* X, _bool TS )

thus ( X = w -succ_of (S,TS) implies S,w ==>* X, _bool TS ) :: thesis: ( S,w ==>* X, _bool TS implies X = w -succ_of (S,TS) )

proof

assume
S,w ==>* X, _bool TS
; :: thesis: X = w -succ_of (S,TS)
assume
X = w -succ_of (S,TS)
; :: thesis: S,w ==>* X, _bool TS

then [[S,w],X] in the Tran of (_bool TS) by A1, Def1;

then S,w -->. X, _bool TS by REWRITE3:def 2;

then S,w ==>. X, <%> E, _bool TS by REWRITE3:23;

then S,w ==>* X, <%> E, _bool TS by REWRITE3:87;

hence S,w ==>* X, _bool TS by REWRITE3:def 7; :: thesis: verum

end;then [[S,w],X] in the Tran of (_bool TS) by A1, Def1;

then S,w -->. X, _bool TS by REWRITE3:def 2;

then S,w ==>. X, <%> E, _bool TS by REWRITE3:23;

then S,w ==>* X, <%> E, _bool TS by REWRITE3:87;

hence S,w ==>* X, _bool TS by REWRITE3:def 7; :: thesis: verum

then A2: S,w ==>* X, <%> E, _bool TS by REWRITE3:def 7;

ex e being Element of E st

( w = <%e%> & w . 0 = e ) by A1, Th4;

then S,w ^ {} ==>. X, <%> E, _bool TS by A2, Th12;

then A3: S,w -->. X, _bool TS by REWRITE3:24;

then X in _bool TS by REWRITE3:15;

then X in the carrier of (_bool TS) ;

then reconsider X9 = X as Subset of TS by Def1;

[[S,w],X9] in the Tran of (_bool TS) by A3, REWRITE3:def 2;

hence X = w -succ_of (S,TS) by Def1; :: thesis: verum