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

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

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

proof

per cases ( w ==>. t1,S or w ==>. t1,{[s,t]} ) by A11, Th21;

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 A1, Th44; :: 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 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;

end;

end;

end;

A13: S₁[ 0 ] by REWRITE1:def 2;
for k being Nat holds S₁[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