let E be set ; :: thesis: for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s ==>. t,S holds
(u ^ s) ^ v ==>. (u ^ t) ^ v,S
let S be semi-Thue-system of E; :: thesis: for s, t, u, v being Element of E ^omega st s ==>. t,S holds
(u ^ s) ^ v ==>. (u ^ t) ^ v,S
let s, t, u, v be Element of E ^omega ; :: thesis: ( s ==>. t,S implies (u ^ s) ^ v ==>. (u ^ t) ^ v,S )
assume s ==>. t,S ; :: thesis: (u ^ s) ^ v ==>. (u ^ t) ^ v,S
then u ^ s ==>. u ^ t,S by Th12;
hence (u ^ s) ^ v ==>. (u ^ t) ^ v,S by Th12; :: thesis: verum