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 S1[ 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 );
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 \/ {[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 )

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

then k = 0 by Th1;
then p = <*s1*> by ;
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;
suppose not k + 1 in dom p ; :: thesis: ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 )

then 0 + 1 > k + 1 by ;
hence ex q being RedSequence of ==>.-relation S st
( q . 1 = s1 & q . (len q) = t1 ) 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 = s1 & q . (len q) = t1 )

set w = p . k;
A10: [(p . k),(p . (k + 1))] in ==>.-relation (S \/ {[s,t]}) by ;
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
proof
per cases ( w ==>. t1,S or w ==>. t1,{[s,t]} ) by ;
suppose w ==>. t1,S ; :: thesis: w ==>* t1,S
hence w ==>* t1,S by Th33; :: thesis: verum
end;
suppose w ==>. t1,{[s,t]} ; :: thesis: w ==>* t1,S
hence w ==>* t1,S by ; :: thesis: verum
end;
end;
end;
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 ;
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;
end;
end;
end;
A13: S1[ 0 ] by REWRITE1:def 2;
for k being Nat holds S1[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