let E be set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( s ==>* t,S \/ (id (E ^omega)) implies s ==>* t,S )

assume s ==>* t,S \/ (id (E ^omega)) ; :: thesis: 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 ; :: thesis: verum

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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( s ==>* t,S \/ (id (E ^omega)) implies s ==>* t,S )

assume s ==>* t,S \/ (id (E ^omega)) ; :: thesis: 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 ; :: thesis: verum