let E be set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( s ==>* t,S implies S,S \/ {[s,t]} are_equivalent_wrt w )

assume A1: s ==>* t,S ; :: thesis: S,S \/ {[s,t]} are_equivalent_wrt w

A2: Lang (w,(S \/ {[s,t]})) c= Lang (w,S)

hence Lang (w,S) = Lang (w,(S \/ {[s,t]})) by A2, XBOOLE_0:def 10; :: according to REWRITE2:def 9 :: thesis: verum

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; :: thesis: 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 ; :: thesis: ( s ==>* t,S implies S,S \/ {[s,t]} are_equivalent_wrt w )

assume A1: s ==>* t,S ; :: thesis: S,S \/ {[s,t]} are_equivalent_wrt w

A2: Lang (w,(S \/ {[s,t]})) c= Lang (w,S)

proof

Lang (w,S) c= Lang (w,(S \/ {[s,t]}))
by Th48, XBOOLE_1:7;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lang (w,(S \/ {[s,t]})) or x in Lang (w,S) )

assume A3: x in Lang (w,(S \/ {[s,t]})) ; :: thesis: x in Lang (w,S)

reconsider u = x as Element of E ^omega by A3;

w ==>* u,S \/ {[s,t]} by A3, Th46;

then w ==>* u,S by A1, Th45;

hence x in Lang (w,S) ; :: thesis: verum

end;assume A3: x in Lang (w,(S \/ {[s,t]})) ; :: thesis: x in Lang (w,S)

reconsider u = x as Element of E ^omega by A3;

w ==>* u,S \/ {[s,t]} by A3, Th46;

then w ==>* u,S by A1, Th45;

hence x in Lang (w,S) ; :: thesis: verum

hence Lang (w,S) = Lang (w,(S \/ {[s,t]})) by A2, XBOOLE_0:def 10; :: according to REWRITE2:def 9 :: thesis: verum