let x, y be set ; :: thesis: for E being non empty set
for u, w, v being Element of E ^omega
for TS being non empty transition-system of (Lex E) \/ {(<%> E)}
for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
let E be non empty set ; :: thesis: for u, w, v being Element of E ^omega
for TS being non empty transition-system of (Lex E) \/ {(<%> E)}
for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
let u, w, v be Element of E ^omega ; :: thesis: for TS being non empty transition-system of (Lex E) \/ {(<%> E)}
for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
let TS be non empty transition-system of (Lex E) \/ {(<%> E)}; :: thesis: for p being RedSequence of ==>.-relation TS st p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] holds
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
let p be RedSequence of ==>.-relation TS; :: thesis: ( p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] implies ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] ) )
assume A:
( p . 1 = [x,(u ^ w)] & p . (len p) = [y,(v ^ w)] )
; :: thesis: ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
deffunc H1( set ) -> set = [((p . $1) `1 ),(chop (dim2 (p . $1),E),w)];
consider q being FinSequence such that
B1:
len q = len p
and
B2:
for k being Nat st k in dom q holds
q . k = H1(k)
from FINSEQ_1:sch 2();
for k being Element of NAT st k in dom q & k + 1 in dom q holds
[(q . k),(q . (k + 1))] in ==>.-relation TS
proof
let k be
Element of
NAT ;
:: thesis: ( k in dom q & k + 1 in dom q implies [(q . k),(q . (k + 1))] in ==>.-relation TS )
assume C1:
(
k in dom q &
k + 1
in dom q )
;
:: thesis: [(q . k),(q . (k + 1))] in ==>.-relation TS
( 1
<= k &
k <= len q & 1
<= k + 1 &
k + 1
<= len q )
by C1, FINSEQ_3:27;
then C2:
(
k in dom p &
k + 1
in dom p )
by B1, FINSEQ_3:27;
consider v1 being
Element of
E ^omega such that D1:
(p . k) `2 = v1 ^ (v ^ w)
by A, C2, REWRITE3:52;
consider v2 being
Element of
E ^omega such that D2:
(p . (k + 1)) `2 = v2 ^ (v ^ w)
by A, C2, REWRITE3:52;
D3:
[(p . k),(p . (k + 1))] in ==>.-relation TS
by C2, REWRITE1:def 2;
then D4:
ex
r1 being
Element of
TS ex
w1 being
Element of
E ^omega ex
r2 being
Element of
TS ex
w2 being
Element of
E ^omega st
(
p . k = [r1,w1] &
p . (k + 1) = [r2,w2] )
by REWRITE3:31;
D5:
dim2 (p . k),
E = v1 ^ (v ^ w)
by D1, D4, REWRITE3:def 5;
D6:
dim2 (p . (k + 1)),
E = v2 ^ (v ^ w)
by D2, D4, REWRITE3:def 5;
[(p . k),[((p . (k + 1)) `1 ),(v2 ^ (v ^ w))]] in ==>.-relation TS
by C2, D2, D3, REWRITE3:48;
then
[[((p . k) `1 ),(v1 ^ (v ^ w))],[((p . (k + 1)) `1 ),(v2 ^ (v ^ w))]] in ==>.-relation TS
by C2, D1, REWRITE3:48;
then
(p . k) `1 ,
v1 ^ (v ^ w) ==>. (p . (k + 1)) `1 ,
v2 ^ (v ^ w),
TS
by REWRITE3:def 4;
then consider u1 being
Element of
E ^omega such that E:
(
(p . k) `1 ,
u1 -->. (p . (k + 1)) `1 ,
TS &
v1 ^ (v ^ w) = u1 ^ (v2 ^ (v ^ w)) )
by REWRITE3:22;
(v1 ^ v) ^ w =
u1 ^ (v2 ^ (v ^ w))
by E, AFINSQ_1:30
.=
(u1 ^ v2) ^ (v ^ w)
by AFINSQ_1:30
.=
((u1 ^ v2) ^ v) ^ w
by AFINSQ_1:30
;
then v1 ^ v =
(u1 ^ v2) ^ v
by AFINSQ_1:31
.=
u1 ^ (v2 ^ v)
by AFINSQ_1:30
;
then F:
(p . k) `1 ,
v1 ^ v ==>. (p . (k + 1)) `1 ,
v2 ^ v,
TS
by E, REWRITE3:def 3;
G1:
q . k =
[((p . k) `1 ),(chop (v1 ^ (v ^ w)),w)]
by B2, C1, D5
.=
[((p . k) `1 ),(chop ((v1 ^ v) ^ w),w)]
by AFINSQ_1:30
.=
[((p . k) `1 ),(v1 ^ v)]
by defCut
;
q . (k + 1) =
[((p . (k + 1)) `1 ),(chop (v2 ^ (v ^ w)),w)]
by B2, C1, D6
.=
[((p . (k + 1)) `1 ),(chop ((v2 ^ v) ^ w),w)]
by AFINSQ_1:30
.=
[((p . (k + 1)) `1 ),(v2 ^ v)]
by defCut
;
hence
[(q . k),(q . (k + 1))] in ==>.-relation TS
by F, G1, REWRITE3:def 4;
:: thesis: verum
end;
then reconsider q = q as RedSequence of ==>.-relation TS by B1, REWRITE1:def 2;
H3:
len p >= 0 + 1
by NAT_1:13;
then H4:
( 1 in dom p & len p in dom p )
by FINSEQ_3:27;
H0:
( 1 in dom q & len p in dom q )
by B1, H3, FINSEQ_3:27;
H1: dim2 (p . 1),E =
(p . 1) `2
by A, H4, REWRITE3:51
.=
u ^ w
by A, MCART_1:7
;
H2: dim2 (p . (len p)),E =
(p . (len p)) `2
by A, H4, REWRITE3:51
.=
v ^ w
by A, MCART_1:7
;
I1: q . 1 =
[((p . 1) `1 ),(chop (dim2 (p . 1),E),w)]
by B2, H0
.=
[x,(chop (u ^ w),w)]
by A, H1, MCART_1:7
.=
[x,u]
by defCut
;
q . (len q) =
[((p . (len p)) `1 ),(chop (dim2 (p . (len p)),E),w)]
by B1, B2, H0
.=
[y,(chop (v ^ w),w)]
by A, H2, MCART_1:7
.=
[y,v]
by defCut
;
hence
ex q being RedSequence of ==>.-relation TS st
( q . 1 = [x,u] & q . (len q) = [y,v] )
by I1; :: thesis: verum