let E be set ; 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; 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 ; ( 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]}
; 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 for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A5:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
let p be
RedSequence of
==>.-relation (S \/ {[s,t]});
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 ;
( 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
;
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 A9:
(
k in dom p &
k + 1
in dom p )
;
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
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;
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
; verum