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
( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
let S be semi-Thue-system of E; :: thesis: 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 ; :: thesis: ( 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 ; :: according to REWRITE2:def 5 :: thesis: ( 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; :: thesis: 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; :: thesis: verum