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