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 A1: ( S is Thue-system of E & s ==>* t,S ) ; :: thesis: t ==>* s,S
then ==>.-relation S reduces s,t by Def7;
then consider p being RedSequence of ==>.-relation S such that
A2: ( p . 1 = s & p . (len p) = t ) by REWRITE1:def 3;
set q = Rev p;
Rev p is RedSequence of (==>.-relation S) ~ by REWRITE1:10;
then A3: Rev p is RedSequence of ==>.-relation S by A1, Th25;
A4: (Rev p) . 1 = t by A2, FINSEQ_5:65;
(Rev p) . (len p) = s by A2, FINSEQ_5:65;
then (Rev p) . (len (Rev p)) = s by FINSEQ_5:def 3;
then ==>.-relation S reduces t,s by A3, A4, REWRITE1:def 3;
hence t ==>* s,S by Def7; :: thesis: verum