let E be set ; :: thesis: for S being semi-Thue-system of E

for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S \/ {[s,t]} holds

u ==>* v,S

let S be semi-Thue-system of E; :: thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S \/ {[s,t]} holds

u ==>* v,S

let s, t, u, v be Element of E ^omega ; :: thesis: ( s ==>* t,S & u ==>* v,S \/ {[s,t]} implies u ==>* v,S )

assume that

A1: s ==>* t,S and

A2: u ==>* v,S \/ {[s,t]} ; :: thesis: u ==>* v,S

==>.-relation (S \/ {[s,t]}) reduces u,v by A2;

then A3: ex p2 being RedSequence of ==>.-relation (S \/ {[s,t]}) st

( p2 . 1 = u & p2 . (len p2) = v ) by REWRITE1:def 3;

defpred S_{1}[ Nat] means for p being RedSequence of ==>.-relation (S \/ {[s,t]})

for s1, t1 being Element of E ^omega st len p = $1 & p . 1 = s1 & p . (len p) = t1 holds

ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = t1 );

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

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A13, A4);

then ex q being RedSequence of ==>.-relation S st

( q . 1 = u & q . (len q) = v ) by A3;

then ==>.-relation S reduces u,v by REWRITE1:def 3;

hence u ==>* v,S ; :: thesis: verum

for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S \/ {[s,t]} holds

u ==>* v,S

let S be semi-Thue-system of E; :: thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S \/ {[s,t]} holds

u ==>* v,S

let s, t, u, v be Element of E ^omega ; :: thesis: ( s ==>* t,S & u ==>* v,S \/ {[s,t]} implies u ==>* v,S )

assume that

A1: s ==>* t,S and

A2: u ==>* v,S \/ {[s,t]} ; :: thesis: u ==>* v,S

==>.-relation (S \/ {[s,t]}) reduces u,v by A2;

then A3: ex p2 being RedSequence of ==>.-relation (S \/ {[s,t]}) st

( p2 . 1 = u & p2 . (len p2) = v ) by REWRITE1:def 3;

defpred S

for s1, t1 being Element of E ^omega st len p = $1 & p . 1 = s1 & p . (len p) = t1 holds

ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = t1 );

A4: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A13:
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 \/ {[s,t]}); :: thesis: for s1, t1 being Element of E ^omega st len p = k + 1 & p . 1 = s1 & p . (len p) = t1 holds

ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = t1 )

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

( q . 1 = s1 & q . (len q) = t1 ) )

assume that

A6: len p = k + 1 and

A7: p . 1 = s1 and

A8: p . (len p) = t1 ; :: thesis: ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = t1 )

end;ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = t1 )

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

( q . 1 = s1 & q . (len q) = t1 ) )

assume that

A6: len p = k + 1 and

A7: p . 1 = s1 and

A8: p . (len p) = t1 ; :: thesis: ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = t1 )

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 = s1 & q . (len q) = t1 )

( q . 1 = s1 & q . (len q) = t1 )

then
k = 0
by Th1;

then p = <*s1*> by A6, A7, FINSEQ_1:40;

then reconsider p = p as RedSequence of ==>.-relation S by REWRITE1:6;

take p ; :: thesis: ( p . 1 = s1 & p . (len p) = t1 )

thus ( p . 1 = s1 & p . (len p) = t1 ) by A7, A8; :: thesis: verum

end;then p = <*s1*> by A6, A7, FINSEQ_1:40;

then reconsider p = p as RedSequence of ==>.-relation S by REWRITE1:6;

take p ; :: thesis: ( p . 1 = s1 & p . (len p) = t1 )

thus ( p . 1 = s1 & p . (len p) = t1 ) by A7, A8; :: thesis: verum

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

( q . 1 = s1 & q . (len q) = t1 )

( q . 1 = s1 & q . (len q) = t1 )

then
0 + 1 > k + 1
by A6, FINSEQ_3:25;

hence ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = t1 ) by XREAL_1:6; :: thesis: verum

end;hence ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = t1 ) 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 = s1 & q . (len q) = t1 )

( q . 1 = s1 & q . (len q) = t1 )

set w = p . k;

A10: [(p . k),(p . (k + 1))] in ==>.-relation (S \/ {[s,t]}) by A9, REWRITE1:def 2;

then reconsider w = p . k as Element of E ^omega by ZFMISC_1:87;

A11: w ==>. t1,S \/ {[s,t]} by A6, A8, A10, Def6;

A12: w ==>* t1,S ex p1 being RedSequence of ==>.-relation (S \/ {[s,t]}) st

( len p1 = k & p1 . 1 = s1 & p1 . (len p1) = w ) by A7, A9, Th4;

then ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = w ) by A5;

then ==>.-relation S reduces s1,w by REWRITE1:def 3;

then s1 ==>* w,S ;

then s1 ==>* t1,S by A12, Th35;

then ==>.-relation S reduces s1,t1 ;

hence ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = t1 ) by REWRITE1:def 3; :: thesis: verum

end;A10: [(p . k),(p . (k + 1))] in ==>.-relation (S \/ {[s,t]}) by A9, REWRITE1:def 2;

then reconsider w = p . k as Element of E ^omega by ZFMISC_1:87;

A11: w ==>. t1,S \/ {[s,t]} by A6, A8, A10, Def6;

A12: w ==>* t1,S ex p1 being RedSequence of ==>.-relation (S \/ {[s,t]}) st

( len p1 = k & p1 . 1 = s1 & p1 . (len p1) = w ) by A7, A9, Th4;

then ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = w ) by A5;

then ==>.-relation S reduces s1,w by REWRITE1:def 3;

then s1 ==>* w,S ;

then s1 ==>* t1,S by A12, Th35;

then ==>.-relation S reduces s1,t1 ;

hence ex q being RedSequence of ==>.-relation S st

( q . 1 = s1 & q . (len q) = t1 ) by REWRITE1:def 3; :: thesis: verum

for k being Nat holds S

then ex q being RedSequence of ==>.-relation S st

( q . 1 = u & q . (len q) = v ) by A3;

then ==>.-relation S reduces u,v by REWRITE1:def 3;

hence u ==>* v,S ; :: thesis: verum