let E be set ; for S being semi-Thue-system of E
for s, t, w being Element of E ^omega st s ==>. t,S holds
S,S \/ {[s,t]} are_equivalent_wrt w
let S be semi-Thue-system of E; for s, t, w being Element of E ^omega st s ==>. t,S holds
S,S \/ {[s,t]} are_equivalent_wrt w
let s, t, w be Element of E ^omega ; ( s ==>. t,S implies S,S \/ {[s,t]} are_equivalent_wrt w )
assume
s ==>. t,S
; S,S \/ {[s,t]} are_equivalent_wrt w
then
[s,t] in ==>.-relation S
by Def6;
then
{[s,t]} c= ==>.-relation S
by ZFMISC_1:31;
then A1:
S \/ {[s,t]} c= S \/ (==>.-relation S)
by XBOOLE_1:9;
( S,S \/ (==>.-relation S) are_equivalent_wrt w & S c= S \/ {[s,t]} )
by Th57, Th60, XBOOLE_1:7;
hence
S,S \/ {[s,t]} are_equivalent_wrt w
by A1, Th56; verum