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 ) )
assume
s -->. t,S
; ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
then
s ==>. t,S
by Th10;
hence
( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
by Th12; verum