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_{1}[ 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 );

_{1}[ 0 ]
by REWRITE1:def 2;

for k being Nat holds S_{1}[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

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

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_{1}[k] holds

S_{1}[k + 1]

A15:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus S_{1}[k + 1]
:: thesis: verum

end;assume A5: S

thus S

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 )

end;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 ) )
;

end;

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 )

( 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;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

suppose
not k + 1 in dom p
; :: thesis: ex q being RedSequence of ==>.-relation S st

( q . 1 = w & q . (len q) = t )

( 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;hence ex q being RedSequence of ==>.-relation S st

( q . 1 = w & q . (len q) = t ) by XREAL_1:6; :: thesis: verum

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 )

( 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 ;

end;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;

end;

suppose
u ==>. t,S
; :: thesis: ex q being RedSequence of ==>.-relation S st

( q . 1 = w & q . (len q) = t )

( 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;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

suppose A13:
u ==>. t,T
; :: thesis: ex q being RedSequence of ==>.-relation S st

( q . 1 = w & q . (len q) = t )

( 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;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

for k being Nat holds S

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