let E be set ; :: thesis: for S being semi-Thue-system of E

for s, t, u being Element of E ^omega st s ==>* t,S holds

( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )

let S be semi-Thue-system of E; :: thesis: for s, t, u being Element of E ^omega st s ==>* t,S holds

( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )

let s, t, u be Element of E ^omega ; :: thesis: ( s ==>* t,S implies ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S ) )

assume s ==>* t,S ; :: thesis: ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )

then ==>.-relation S reduces s,t ;

then consider p being RedSequence of ==>.-relation S such that

A1: p . 1 = s and

A2: p . (len p) = t by REWRITE1:def 3;

reconsider p = p as FinSequence of E ^omega by A1, ABCMIZ_0:73;

1 in dom p by FINSEQ_5:6;

then A3: (p +^ u) . 1 = s ^ u by A1, Def3;

A4: len p = len (p +^ u) by Th5;

then len (p +^ u) in dom p by FINSEQ_5:6;

then A5: (p +^ u) . (len (p +^ u)) = t ^ u by A2, A4, Def3;

p +^ u is RedSequence of ==>.-relation S by Th23;

then ==>.-relation S reduces s ^ u,t ^ u by A3, A5, REWRITE1:def 3;

hence s ^ u ==>* t ^ u,S ; :: thesis: u ^ s ==>* u ^ t,S

1 in dom p by FINSEQ_5:6;

then A6: (u ^+ p) . 1 = u ^ s by A1, Def2;

A7: len p = len (u ^+ p) by Th5;

then len (u ^+ p) in dom p by FINSEQ_5:6;

then A8: (u ^+ p) . (len (u ^+ p)) = u ^ t by A2, A7, Def2;

u ^+ p is RedSequence of ==>.-relation S by Th23;

then ==>.-relation S reduces u ^ s,u ^ t by A6, A8, REWRITE1:def 3;

hence u ^ s ==>* u ^ t,S ; :: thesis: verum

for s, t, u being Element of E ^omega st s ==>* t,S holds

( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )

let S be semi-Thue-system of E; :: thesis: for s, t, u being Element of E ^omega st s ==>* t,S holds

( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )

let s, t, u be Element of E ^omega ; :: thesis: ( s ==>* t,S implies ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S ) )

assume s ==>* t,S ; :: thesis: ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )

then ==>.-relation S reduces s,t ;

then consider p being RedSequence of ==>.-relation S such that

A1: p . 1 = s and

A2: p . (len p) = t by REWRITE1:def 3;

reconsider p = p as FinSequence of E ^omega by A1, ABCMIZ_0:73;

1 in dom p by FINSEQ_5:6;

then A3: (p +^ u) . 1 = s ^ u by A1, Def3;

A4: len p = len (p +^ u) by Th5;

then len (p +^ u) in dom p by FINSEQ_5:6;

then A5: (p +^ u) . (len (p +^ u)) = t ^ u by A2, A4, Def3;

p +^ u is RedSequence of ==>.-relation S by Th23;

then ==>.-relation S reduces s ^ u,t ^ u by A3, A5, REWRITE1:def 3;

hence s ^ u ==>* t ^ u,S ; :: thesis: u ^ s ==>* u ^ t,S

1 in dom p by FINSEQ_5:6;

then A6: (u ^+ p) . 1 = u ^ s by A1, Def2;

A7: len p = len (u ^+ p) by Th5;

then len (u ^+ p) in dom p by FINSEQ_5:6;

then A8: (u ^+ p) . (len (u ^+ p)) = u ^ t by A2, A7, Def2;

u ^+ p is RedSequence of ==>.-relation S by Th23;

then ==>.-relation S reduces u ^ s,u ^ t by A6, A8, REWRITE1:def 3;

hence u ^ s ==>* u ^ t,S ; :: thesis: verum