let E be non empty set ; for u, v being Element of E ^omega
for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for p, q being Element of TS st p,u ^ v ==>* q,TS holds
ex r being Element of TS st
( p,u ==>* r,TS & r,v ==>* q,TS )
let u, v be Element of E ^omega ; for TS being non empty transition-system over (Lex E) \/ {(<%> E)}
for p, q being Element of TS st p,u ^ v ==>* q,TS holds
ex r being Element of TS st
( p,u ==>* r,TS & r,v ==>* q,TS )
let TS be non empty transition-system over (Lex E) \/ {(<%> E)}; for p, q being Element of TS st p,u ^ v ==>* q,TS holds
ex r being Element of TS st
( p,u ==>* r,TS & r,v ==>* q,TS )
let p, q be Element of TS; ( p,u ^ v ==>* q,TS implies ex r being Element of TS st
( p,u ==>* r,TS & r,v ==>* q,TS ) )
assume A1:
p,u ^ v ==>* q,TS
; ex r being Element of TS st
( p,u ==>* r,TS & r,v ==>* q,TS )
then
p,u ^ v ==>* q, <%> E,TS
by REWRITE3:def 7;
then
==>.-relation TS reduces [p,(u ^ v)],[q,(<%> E)]
by REWRITE3:def 6;
then consider R being RedSequence of ==>.-relation TS such that
A2:
R . 1 = [p,(u ^ v)]
and
A3:
R . (len R) = [q,(<%> E)]
by REWRITE1:def 3;
A4:
(R . (len R)) `2 = <%> E
by A3;
(R . 1) `2 = u ^ v
by A2;
then consider l being Nat such that
A5:
l in dom R
and
A6:
(R . l) `2 = v
by A4, Th24;
per cases
( l + 1 in dom R or not l + 1 in dom R )
;
suppose A7:
l + 1
in dom R
;
ex r being Element of TS st
( p,u ==>* r,TS & r,v ==>* q,TS )then
(R . l) `1 in TS
by A5, REWRITE3:49;
then reconsider r =
(R . l) `1 as
Element of
TS ;
A8:
R . l = [r,v]
by A5, A6, A7, REWRITE3:48;
A9:
l <= len R
by A5, FINSEQ_3:25;
take
r
;
( p,u ==>* r,TS & r,v ==>* q,TS )A10:
( 1
in dom R & 1
<= l )
by A5, FINSEQ_3:25, FINSEQ_5:6;
reconsider l =
l as
Element of
NAT by ORDINAL1:def 12;
==>.-relation TS reduces R . 1,
R . l
by A5, A10, REWRITE1:17;
then
p,
u ^ v ==>* r,
{} ^ v,
TS
by A2, A8, REWRITE3:def 6;
then
p,
u ==>* r,
<%> E,
TS
by Th27;
hence
p,
u ==>* r,
TS
by REWRITE3:def 7;
r,v ==>* q,TS
0 + 1
<= len R
by NAT_1:13;
then
len R in dom R
by FINSEQ_3:25;
then
==>.-relation TS reduces R . l,
R . (len R)
by A5, A9, REWRITE1:17;
then
r,
v ==>* q,
<%> E,
TS
by A3, A8, REWRITE3:def 6;
hence
r,
v ==>* q,
TS
by REWRITE3:def 7;
verum end;