let E be set ; 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; 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 ; ( 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
; REWRITE2:def 9 ==>.-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 S1[ 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 );
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 \/ T);
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 ;
( 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
;
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 ) )
;
suppose A9:
(
k in dom p &
k + 1
in dom p )
;
ex q being RedSequence of ==>.-relation S st
( 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
;
per cases
( u ==>. t,S or u ==>. t,T )
by A11, Th21;
suppose A13:
u ==>. t,
T
;
ex q being RedSequence of ==>.-relation S st
( 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;
verum end; end; end; end;
end; end;
A15:
S1[ 0 ]
by REWRITE1:def 2;
for k being Nat holds S1[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; verum