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
( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
let S be semi-Thue-system of E; for s, t, u being Element of E ^omega st s ==>. t,S holds
( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
let s, t, u be Element of E ^omega ; ( s ==>. t,S implies ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) )
given v, w, s1, t1 being Element of E ^omega such that A1:
s = (v ^ s1) ^ w
and
A2:
t = (v ^ t1) ^ w
and
A3:
s1 -->. t1,S
; REWRITE2:def 5 ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
A4: u ^ t =
(u ^ (v ^ t1)) ^ w
by A2, AFINSQ_1:27
.=
((u ^ v) ^ t1) ^ w
by AFINSQ_1:27
;
u ^ s =
(u ^ (v ^ s1)) ^ w
by A1, AFINSQ_1:27
.=
((u ^ v) ^ s1) ^ w
by AFINSQ_1:27
;
hence
u ^ s ==>. u ^ t,S
by A3, A4; s ^ u ==>. t ^ u,S
( s ^ u = (v ^ s1) ^ (w ^ u) & t ^ u = (v ^ t1) ^ (w ^ u) )
by A1, A2, AFINSQ_1:27;
hence
s ^ u ==>. t ^ u,S
by A3; verum