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: ==>.-relation S reduces w,s
A3: ex p being RedSequence of ==>.-relation (S \/ T) st
( p . 1 = w & p . (len p) = s ) by A2, REWRITE1:def 3;
defpred S₁[ 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 S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[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 A6, A7, FINSEQ_1:40;
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 A6, FINSEQ_3:25;
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 A9, REWRITE1:def 2;
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 A11, Th21;

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

then u ==>* t,S by Th33;
then w ==>* t,S by A12, Th35;
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;

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 A1, Th46;
u ==>* t,T by A13, Th33;
then w ==>* t,T by A14, Th35;
then t in Lang (w,T) ;
then w ==>* t,S by A1, Th46;
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: S₁[ 0 ] by REWRITE1:def 2;
for k being Nat holds S₁[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