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