let E be set ; :: thesis: for S, T being semi-Thue-system of E
for w, s 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 w, s 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 w, s 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
consider p being RedSequence of ==>.-relation (S \/ T) such that
A3: ( 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: S₁[ 0 ] by REWRITE1:def 2;

A5: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: 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 A7: ( len p = k + 1 & p . 1 = w & 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 A7, FINSEQ_1:57;
then reconsider p = p as RedSequence of ==>.-relation S by REWRITE1:7;
take p ; :: thesis: ( p . 1 = w & p . (len p) = t )
thus ( p . 1 = w & p . (len p) = t ) by A7; :: 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 A7, FINSEQ_3:27;
hence ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t ) by XREAL_1:8; :: thesis: verum

end;

suppose A8: ( 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 A9: [(p . k),(p . (k + 1))] in ==>.-relation (S \/ T) by REWRITE1:def 2;
set u = p . k;
reconsider u = p . k as Element of E ^omega by A9, ZFMISC_1:106;
A10: u ==>. t,S \/ T by A7, A9, Def6;
consider p1 being RedSequence of ==>.-relation (S \/ T) such that
A11: ( len p1 = k & p1 . 1 = w & p1 . (len p1) = u ) by A7, A8, Th4;
consider q being RedSequence of ==>.-relation S such that
A12: ( q . 1 = w & q . (len q) = u ) by A6, A11;
==>.-relation S reduces w,u by A12, REWRITE1:def 3;
then A13: w ==>* u,S by Def7;

per cases ( u ==>. t,S or u ==>. t,T ) by A10, 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 A13, Th35;
then ==>.-relation S reduces w,t by Def7;
hence ex q being RedSequence of ==>.-relation S st
( q . 1 = w & q . (len q) = t ) by REWRITE1:def 3; :: thesis: verum

end;

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

then A14: u ==>* t,T by Th33;
u in Lang w,S by A13;
then w ==>* u,T by A1, Th46;
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 by Def7;
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;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
then consider q being RedSequence of ==>.-relation S such that
A15: ( q . 1 = w & q . (len q) = s ) by A3;
thus ==>.-relation S reduces w,s by A15, REWRITE1:def 3; :: thesis: verum