let E be set ; for S being semi-Thue-system of E
for s, t being Element of E ^omega holds
( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega)) )
let S be semi-Thue-system of E; for s, t being Element of E ^omega holds
( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega)) )
let s, t be Element of E ^omega ; ( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega)) )
thus
( s ==>* t,S implies s ==>* t,S \/ (id (E ^omega)) )
by Th40, XBOOLE_1:7; ( s ==>* t,S \/ (id (E ^omega)) implies s ==>* t,S )
assume
s ==>* t,S \/ (id (E ^omega))
; s ==>* t,S
then
==>.-relation (S \/ (id (E ^omega))) reduces s,t
;
then
(==>.-relation S) \/ (id (E ^omega)) reduces s,t
by Th28;
then
==>.-relation S reduces s,t
by REWRITE1:23;
hence
s ==>* t,S
; verum