let E be set ; :: thesis: for S, T being semi-Thue-system of E
for s, w being Element of E ^omega st S,T are_equivalent_wrt w & ==>.-relation (S \/ T) reduces w,s holds
==>.-relation S reduces w,s

let S, T be semi-Thue-system of E; :: thesis: for s, w being Element of E ^omega st S,T are_equivalent_wrt w & ==>.-relation (S \/ T) reduces w,s holds
==>.-relation S reduces w,s

let s, w be Element of E ^omega ; :: thesis: ( S,T are_equivalent_wrt w & ==>.-relation (S \/ T) reduces w,s implies ==>.-relation S reduces w,s )
assume that
A1: Lang (w,S) = Lang (w,T) and
A2: ==>.-relation (S \/ T) reduces w,s ; :: according to REWRITE2:def 9 :: thesis:
A3: ex p being RedSequence of ==>.-relation (S \/ T) st
( p . 1 = w & p . (len p) = s ) by ;
defpred S1[ Nat] means for p being RedSequence of ==>.-relation (S \/ T)
for t being Element of E ^omega st len p = \$1 & p . 1 = w & p . (len p) = t holds
ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t );
A4: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
proof
let p be RedSequence of ==>.-relation (S \/ T); :: thesis: for t being Element of E ^omega st len p = k + 1 & p . 1 = w & p . (len p) = t holds
ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )

let t be Element of E ^omega ; :: thesis: ( len p = k + 1 & p . 1 = w & p . (len p) = t implies ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t ) )

assume that
A6: len p = k + 1 and
A7: p . 1 = w and
A8: p . (len p) = t ; :: thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )

per cases ( ( not k in dom p & k + 1 in dom p ) or not k + 1 in dom p or ( k in dom p & k + 1 in dom p ) ) ;
suppose ( not k in dom p & k + 1 in dom p ) ; :: thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )

then k = 0 by Th1;
then p = <*w*> by ;
then reconsider p = p as RedSequence of ==>.-relation S by REWRITE1:6;
take p ; :: thesis: ( p . 1 = w & p . (len p) = t )
thus ( p . 1 = w & p . (len p) = t ) by A7, A8; :: thesis: verum
end;
suppose not k + 1 in dom p ; :: thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )

then 0 + 1 > k + 1 by ;
hence ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t ) by XREAL_1:6; :: thesis: verum
end;
suppose A9: ( k in dom p & k + 1 in dom p ) ; :: thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )

set u = p . k;
A10: [(p . k),(p . (k + 1))] in ==>.-relation (S \/ T) by ;
then reconsider u = p . k as Element of E ^omega by ZFMISC_1:87;
A11: u ==>. t,S \/ T by A6, A8, A10, Def6;
ex p1 being RedSequence of ==>.-relation (S \/ T) st
( len p1 = k & p1 . 1 = w & p1 . (len p1) = u ) by A7, A9, Th4;
then ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = u ) by A5;
then ==>.-relation S reduces w,u by REWRITE1:def 3;
then A12: w ==>* u,S ;
per cases ( u ==>. t,S or u ==>. t,T ) by ;
suppose u ==>. t,S ; :: thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )

end;
suppose A13: u ==>. t,T ; :: thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t )

u in Lang (w,S) by A12;
then A14: w ==>* u,T by ;
u ==>* t,T by ;
then w ==>* t,T by ;
then t in Lang (w,T) ;
then w ==>* t,S by ;
then ==>.-relation S reduces w,t ;
hence ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t ) by REWRITE1:def 3; :: thesis: verum
end;
end;
end;
end;
end;
end;
A15: S1[ 0 ] by REWRITE1:def 2;
for k being Nat holds S1[k] from NAT_1:sch 2(A15, A4);
then ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = s ) by A3;
hence ==>.-relation S reduces w,s by REWRITE1:def 3; :: thesis: verum