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, Def7;
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:65;
then A5: (Rev p) . (len (Rev p)) = s by FINSEQ_5:def 3;
Rev p is RedSequence of (==>.-relation S) ~ by REWRITE1:10;
then A6: Rev p is RedSequence of ==>.-relation S by A1, Th25;
(Rev p) . 1 = t by A4, FINSEQ_5:65;
then ==>.-relation S reduces t,s by A6, A5, REWRITE1:def 3;
hence t ==>* s,S by Def7; :: thesis: verum