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

for s, t being Element of E ^omega st S is Thue-system of E & s ==>* t,S holds

t ==>* s,S

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

t ==>* s,S

let s, t be Element of E ^omega ; :: thesis: ( S is Thue-system of E & s ==>* t,S implies t ==>* s,S )

assume that

A1: S is Thue-system of E and

A2: s ==>* t,S ; :: thesis: t ==>* s,S

==>.-relation S reduces s,t by A2;

then consider p being RedSequence of ==>.-relation S such that

A3: p . 1 = s and

A4: p . (len p) = t by REWRITE1:def 3;

set q = Rev p;

(Rev p) . (len p) = s by A3, FINSEQ_5:62;

then A5: (Rev p) . (len (Rev p)) = s by FINSEQ_5:def 3;

Rev p is RedSequence of (==>.-relation S) ~ by REWRITE1:9;

then A6: Rev p is RedSequence of ==>.-relation S by A1, Th25;

(Rev p) . 1 = t by A4, FINSEQ_5:62;

then ==>.-relation S reduces t,s by A6, A5, REWRITE1:def 3;

hence t ==>* s,S ; :: thesis: verum

for s, t being Element of E ^omega st S is Thue-system of E & s ==>* t,S holds

t ==>* s,S

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

t ==>* s,S

let s, t be Element of E ^omega ; :: thesis: ( S is Thue-system of E & s ==>* t,S implies t ==>* s,S )

assume that

A1: S is Thue-system of E and

A2: s ==>* t,S ; :: thesis: t ==>* s,S

==>.-relation S reduces s,t by A2;

then consider p being RedSequence of ==>.-relation S such that

A3: p . 1 = s and

A4: p . (len p) = t by REWRITE1:def 3;

set q = Rev p;

(Rev p) . (len p) = s by A3, FINSEQ_5:62;

then A5: (Rev p) . (len (Rev p)) = s by FINSEQ_5:def 3;

Rev p is RedSequence of (==>.-relation S) ~ by REWRITE1:9;

then A6: Rev p is RedSequence of ==>.-relation S by A1, Th25;

(Rev p) . 1 = t by A4, FINSEQ_5:62;

then ==>.-relation S reduces t,s by A6, A5, REWRITE1:def 3;

hence t ==>* s,S ; :: thesis: verum