set cTS = bool the carrier of TS;

defpred S_{1}[ set , set ] means for c being Element of bool the carrier of TS

for i being Element of E ^omega st $1 = [c,i] holds

( len i = 1 & $2 = i -succ_of (c,TS) );

consider tTS being Relation of [:(bool the carrier of TS),(Lex E):],(bool the carrier of TS) such that

A1: for x being Element of [:(bool the carrier of TS),(Lex E):]

for y being Element of bool the carrier of TS holds

( [x,y] in tTS iff S_{1}[x,y] )
from RELSET_1:sch 2();

set bTS = transition-system(# (bool the carrier of TS),tTS #);

reconsider bTS = transition-system(# (bool the carrier of TS),tTS #) as strict transition-system over Lex E ;

take bTS ; :: thesis: ( the carrier of bTS = bool the carrier of TS & ( for S being Subset of TS

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) )

thus the carrier of bTS = bool the carrier of TS ; :: thesis: for S being Subset of TS

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )

let S be Subset of TS; :: thesis: for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )

let w be Element of E ^omega ; :: thesis: for T being Subset of TS holds

( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )

let T be Subset of TS; :: thesis: ( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )

thus ( [[S,w],T] in the Tran of bTS implies ( len w = 1 & T = w -succ_of (S,TS) ) ) :: thesis: ( len w = 1 & T = w -succ_of (S,TS) implies [[S,w],T] in the Tran of bTS )

assume that

A3: len w = 1 and

A4: T = w -succ_of (S,TS) ; :: thesis: [[S,w],T] in the Tran of bTS

then reconsider x = [S,w] as Element of [:(bool the carrier of TS),(Lex E):] by ZFMISC_1:87;

[x,T] in tTS by A1, A5;

hence [[S,w],T] in the Tran of bTS ; :: thesis: verum

defpred S

for i being Element of E ^omega st $1 = [c,i] holds

( len i = 1 & $2 = i -succ_of (c,TS) );

consider tTS being Relation of [:(bool the carrier of TS),(Lex E):],(bool the carrier of TS) such that

A1: for x being Element of [:(bool the carrier of TS),(Lex E):]

for y being Element of bool the carrier of TS holds

( [x,y] in tTS iff S

set bTS = transition-system(# (bool the carrier of TS),tTS #);

reconsider bTS = transition-system(# (bool the carrier of TS),tTS #) as strict transition-system over Lex E ;

take bTS ; :: thesis: ( the carrier of bTS = bool the carrier of TS & ( for S being Subset of TS

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) ) ) )

thus the carrier of bTS = bool the carrier of TS ; :: thesis: for S being Subset of TS

for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )

let S be Subset of TS; :: thesis: for w being Element of E ^omega

for T being Subset of TS holds

( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )

let w be Element of E ^omega ; :: thesis: for T being Subset of TS holds

( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )

let T be Subset of TS; :: thesis: ( [[S,w],T] in the Tran of bTS iff ( len w = 1 & T = w -succ_of (S,TS) ) )

thus ( [[S,w],T] in the Tran of bTS implies ( len w = 1 & T = w -succ_of (S,TS) ) ) :: thesis: ( len w = 1 & T = w -succ_of (S,TS) implies [[S,w],T] in the Tran of bTS )

proof

set x = [S,w];
assume A2:
[[S,w],T] in the Tran of bTS
; :: thesis: ( len w = 1 & T = w -succ_of (S,TS) )

then reconsider xc = [S,w] as Element of [:(bool the carrier of TS),(Lex E):] by ZFMISC_1:87;

[xc,T] in tTS by A2;

hence ( len w = 1 & T = w -succ_of (S,TS) ) by A1; :: thesis: verum

end;then reconsider xc = [S,w] as Element of [:(bool the carrier of TS),(Lex E):] by ZFMISC_1:87;

[xc,T] in tTS by A2;

hence ( len w = 1 & T = w -succ_of (S,TS) ) by A1; :: thesis: verum

assume that

A3: len w = 1 and

A4: T = w -succ_of (S,TS) ; :: thesis: [[S,w],T] in the Tran of bTS

A5: now :: thesis: for xc being Element of bool the carrier of TS

for xi being Element of E ^omega st [S,w] = [xc,xi] holds

( len xi = 1 & T = xi -succ_of (xc,TS) )

w in Lex E
by A3, Th9;for xi being Element of E ^omega st [S,w] = [xc,xi] holds

( len xi = 1 & T = xi -succ_of (xc,TS) )

let xc be Element of bool the carrier of TS; :: thesis: for xi being Element of E ^omega st [S,w] = [xc,xi] holds

( len xi = 1 & T = xi -succ_of (xc,TS) )

let xi be Element of E ^omega ; :: thesis: ( [S,w] = [xc,xi] implies ( len xi = 1 & T = xi -succ_of (xc,TS) ) )

assume A6: [S,w] = [xc,xi] ; :: thesis: ( len xi = 1 & T = xi -succ_of (xc,TS) )

xc = S by A6, XTUPLE_0:1;

hence ( len xi = 1 & T = xi -succ_of (xc,TS) ) by A3, A4, A6, XTUPLE_0:1; :: thesis: verum

end;( len xi = 1 & T = xi -succ_of (xc,TS) )

let xi be Element of E ^omega ; :: thesis: ( [S,w] = [xc,xi] implies ( len xi = 1 & T = xi -succ_of (xc,TS) ) )

assume A6: [S,w] = [xc,xi] ; :: thesis: ( len xi = 1 & T = xi -succ_of (xc,TS) )

xc = S by A6, XTUPLE_0:1;

hence ( len xi = 1 & T = xi -succ_of (xc,TS) ) by A3, A4, A6, XTUPLE_0:1; :: thesis: verum

then reconsider x = [S,w] as Element of [:(bool the carrier of TS),(Lex E):] by ZFMISC_1:87;

[x,T] in tTS by A1, A5;

hence [[S,w],T] in the Tran of bTS ; :: thesis: verum