let E be set ; 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; 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 ; ( s ==>* t,S implies ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S ) )
assume
s ==>* t,S
; ( 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
; 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
; verum