let E be set ; :: thesis: for S being semi-Thue-system of E

for s, t being Element of E ^omega st s -->. t,S holds

s ==>. t,S

let S be semi-Thue-system of E; :: thesis: for s, t being Element of E ^omega st s -->. t,S holds

s ==>. t,S

let s, t be Element of E ^omega ; :: thesis: ( s -->. t,S implies s ==>. t,S )

assume A1: s -->. t,S ; :: thesis: s ==>. t,S

take e = <%> E; :: according to REWRITE2:def 5 :: thesis: ex w, s1, t1 being Element of E ^omega st

( s = (e ^ s1) ^ w & t = (e ^ t1) ^ w & s1 -->. t1,S )

A2: t = ({} ^ t) ^ {}

.= (e ^ t) ^ e ;

s = ({} ^ s) ^ {}

.= (e ^ s) ^ e ;

hence ex w, s1, t1 being Element of E ^omega st

( s = (e ^ s1) ^ w & t = (e ^ t1) ^ w & s1 -->. t1,S ) by A1, A2; :: thesis: verum

for s, t being Element of E ^omega st s -->. t,S holds

s ==>. t,S

let S be semi-Thue-system of E; :: thesis: for s, t being Element of E ^omega st s -->. t,S holds

s ==>. t,S

let s, t be Element of E ^omega ; :: thesis: ( s -->. t,S implies s ==>. t,S )

assume A1: s -->. t,S ; :: thesis: s ==>. t,S

take e = <%> E; :: according to REWRITE2:def 5 :: thesis: ex w, s1, t1 being Element of E ^omega st

( s = (e ^ s1) ^ w & t = (e ^ t1) ^ w & s1 -->. t1,S )

A2: t = ({} ^ t) ^ {}

.= (e ^ t) ^ e ;

s = ({} ^ s) ^ {}

.= (e ^ s) ^ e ;

hence ex w, s1, t1 being Element of E ^omega st

( s = (e ^ s1) ^ w & t = (e ^ t1) ^ w & s1 -->. t1,S ) by A1, A2; :: thesis: verum