let x, y be set ; :: thesis: for E being non empty set

for u, v, w being Element of E ^omega

for TS being non empty transition-system over (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, v, w being Element of E ^omega

for TS being non empty transition-system over (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, v, w be Element of E ^omega ; :: thesis: for TS being non empty transition-system over (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 over (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 that

A1: p . 1 = [x,(u ^ w)] and

A2: p . (len p) = [y,(v ^ w)] ; :: thesis: ex q being RedSequence of ==>.-relation TS st

( q . 1 = [x,u] & q . (len q) = [y,v] )

A3: len p >= 0 + 1 by NAT_1:13;

then 1 in dom p by FINSEQ_3:25;

then A4: dim2 ((p . 1),E) = (p . 1) `2 by A1, REWRITE3:51

.= u ^ w by A1 ;

deffunc H_{1}( set ) -> object = [((p . $1) `1),(chop ((dim2 ((p . $1),E)),w))];

consider q being FinSequence such that

A5: len q = len p and

A6: for k being Nat st k in dom q holds

q . k = H_{1}(k)
from FINSEQ_1:sch 2();

A7: for k being Nat st k in dom q & k + 1 in dom q holds

[(q . k),(q . (k + 1))] in ==>.-relation TS

then A20: dim2 ((p . (len p)),E) = (p . (len p)) `2 by A1, REWRITE3:51

.= v ^ w by A2 ;

reconsider q = q as RedSequence of ==>.-relation TS by A5, A7, REWRITE1:def 2;

1 in dom q by A5, A3, FINSEQ_3:25;

then A21: q . 1 = [((p . 1) `1),(chop ((dim2 ((p . 1),E)),w))] by A6

.= [x,(chop ((u ^ w),w))] by A1, A4

.= [x,u] by Def9 ;

len p in dom q by A5, A3, FINSEQ_3:25;

then q . (len q) = [((p . (len p)) `1),(chop ((dim2 ((p . (len p)),E)),w))] by A5, A6

.= [y,(chop ((v ^ w),w))] by A2, A20

.= [y,v] by Def9 ;

hence ex q being RedSequence of ==>.-relation TS st

( q . 1 = [x,u] & q . (len q) = [y,v] ) by A21; :: thesis: verum

for u, v, w being Element of E ^omega

for TS being non empty transition-system over (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, v, w being Element of E ^omega

for TS being non empty transition-system over (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, v, w be Element of E ^omega ; :: thesis: for TS being non empty transition-system over (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 over (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 that

A1: p . 1 = [x,(u ^ w)] and

A2: p . (len p) = [y,(v ^ w)] ; :: thesis: ex q being RedSequence of ==>.-relation TS st

( q . 1 = [x,u] & q . (len q) = [y,v] )

A3: len p >= 0 + 1 by NAT_1:13;

then 1 in dom p by FINSEQ_3:25;

then A4: dim2 ((p . 1),E) = (p . 1) `2 by A1, REWRITE3:51

.= u ^ w by A1 ;

deffunc H

consider q being FinSequence such that

A5: len q = len p and

A6: for k being Nat st k in dom q holds

q . k = H

A7: for k being Nat st k in dom q & k + 1 in dom q holds

[(q . k),(q . (k + 1))] in ==>.-relation TS

proof

len p in dom p
by A3, FINSEQ_3:25;
let k be Nat; :: thesis: ( k in dom q & k + 1 in dom q implies [(q . k),(q . (k + 1))] in ==>.-relation TS )

assume that

A8: k in dom q and

A9: k + 1 in dom q ; :: thesis: [(q . k),(q . (k + 1))] in ==>.-relation TS

( 1 <= k & k <= len q ) by A8, FINSEQ_3:25;

then A10: k in dom p by A5, FINSEQ_3:25;

then consider v1 being Element of E ^omega such that

A11: (p . k) `2 = v1 ^ (v ^ w) by A2, REWRITE3:52;

( 1 <= k + 1 & k + 1 <= len q ) by A9, FINSEQ_3:25;

then A12: k + 1 in dom p by A5, FINSEQ_3:25;

then consider v2 being Element of E ^omega such that

A13: (p . (k + 1)) `2 = v2 ^ (v ^ w) by A2, REWRITE3:52;

A14: [(p . k),(p . (k + 1))] in ==>.-relation TS by A10, A12, REWRITE1:def 2;

then [(p . k),[((p . (k + 1)) `1),(v2 ^ (v ^ w))]] in ==>.-relation TS by A10, A12, A13, REWRITE3:48;

then [[((p . k) `1),(v1 ^ (v ^ w))],[((p . (k + 1)) `1),(v2 ^ (v ^ w))]] in ==>.-relation TS by A10, A12, A11, 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

A15: (p . k) `1 ,u1 -->. (p . (k + 1)) `1 ,TS and

A16: v1 ^ (v ^ w) = u1 ^ (v2 ^ (v ^ w)) by REWRITE3:22;

A17: 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 A14, REWRITE3:31;

then dim2 ((p . (k + 1)),E) = v2 ^ (v ^ w) by A13, REWRITE3:def 5;

then A18: q . (k + 1) = [((p . (k + 1)) `1),(chop ((v2 ^ (v ^ w)),w))] by A6, A9

.= [((p . (k + 1)) `1),(chop (((v2 ^ v) ^ w),w))] by AFINSQ_1:27

.= [((p . (k + 1)) `1),(v2 ^ v)] by Def9 ;

(v1 ^ v) ^ w = u1 ^ (v2 ^ (v ^ w)) by A16, AFINSQ_1:27

.= (u1 ^ v2) ^ (v ^ w) by AFINSQ_1:27

.= ((u1 ^ v2) ^ v) ^ w by AFINSQ_1:27 ;

then v1 ^ v = (u1 ^ v2) ^ v by AFINSQ_1:28

.= u1 ^ (v2 ^ v) by AFINSQ_1:27 ;

then A19: (p . k) `1 ,v1 ^ v ==>. (p . (k + 1)) `1 ,v2 ^ v,TS by A15, REWRITE3:def 3;

dim2 ((p . k),E) = v1 ^ (v ^ w) by A11, A17, REWRITE3:def 5;

then q . k = [((p . k) `1),(chop ((v1 ^ (v ^ w)),w))] by A6, A8

.= [((p . k) `1),(chop (((v1 ^ v) ^ w),w))] by AFINSQ_1:27

.= [((p . k) `1),(v1 ^ v)] by Def9 ;

hence [(q . k),(q . (k + 1))] in ==>.-relation TS by A19, A18, REWRITE3:def 4; :: thesis: verum

end;assume that

A8: k in dom q and

A9: k + 1 in dom q ; :: thesis: [(q . k),(q . (k + 1))] in ==>.-relation TS

( 1 <= k & k <= len q ) by A8, FINSEQ_3:25;

then A10: k in dom p by A5, FINSEQ_3:25;

then consider v1 being Element of E ^omega such that

A11: (p . k) `2 = v1 ^ (v ^ w) by A2, REWRITE3:52;

( 1 <= k + 1 & k + 1 <= len q ) by A9, FINSEQ_3:25;

then A12: k + 1 in dom p by A5, FINSEQ_3:25;

then consider v2 being Element of E ^omega such that

A13: (p . (k + 1)) `2 = v2 ^ (v ^ w) by A2, REWRITE3:52;

A14: [(p . k),(p . (k + 1))] in ==>.-relation TS by A10, A12, REWRITE1:def 2;

then [(p . k),[((p . (k + 1)) `1),(v2 ^ (v ^ w))]] in ==>.-relation TS by A10, A12, A13, REWRITE3:48;

then [[((p . k) `1),(v1 ^ (v ^ w))],[((p . (k + 1)) `1),(v2 ^ (v ^ w))]] in ==>.-relation TS by A10, A12, A11, 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

A15: (p . k) `1 ,u1 -->. (p . (k + 1)) `1 ,TS and

A16: v1 ^ (v ^ w) = u1 ^ (v2 ^ (v ^ w)) by REWRITE3:22;

A17: 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 A14, REWRITE3:31;

then dim2 ((p . (k + 1)),E) = v2 ^ (v ^ w) by A13, REWRITE3:def 5;

then A18: q . (k + 1) = [((p . (k + 1)) `1),(chop ((v2 ^ (v ^ w)),w))] by A6, A9

.= [((p . (k + 1)) `1),(chop (((v2 ^ v) ^ w),w))] by AFINSQ_1:27

.= [((p . (k + 1)) `1),(v2 ^ v)] by Def9 ;

(v1 ^ v) ^ w = u1 ^ (v2 ^ (v ^ w)) by A16, AFINSQ_1:27

.= (u1 ^ v2) ^ (v ^ w) by AFINSQ_1:27

.= ((u1 ^ v2) ^ v) ^ w by AFINSQ_1:27 ;

then v1 ^ v = (u1 ^ v2) ^ v by AFINSQ_1:28

.= u1 ^ (v2 ^ v) by AFINSQ_1:27 ;

then A19: (p . k) `1 ,v1 ^ v ==>. (p . (k + 1)) `1 ,v2 ^ v,TS by A15, REWRITE3:def 3;

dim2 ((p . k),E) = v1 ^ (v ^ w) by A11, A17, REWRITE3:def 5;

then q . k = [((p . k) `1),(chop ((v1 ^ (v ^ w)),w))] by A6, A8

.= [((p . k) `1),(chop (((v1 ^ v) ^ w),w))] by AFINSQ_1:27

.= [((p . k) `1),(v1 ^ v)] by Def9 ;

hence [(q . k),(q . (k + 1))] in ==>.-relation TS by A19, A18, REWRITE3:def 4; :: thesis: verum

then A20: dim2 ((p . (len p)),E) = (p . (len p)) `2 by A1, REWRITE3:51

.= v ^ w by A2 ;

reconsider q = q as RedSequence of ==>.-relation TS by A5, A7, REWRITE1:def 2;

1 in dom q by A5, A3, FINSEQ_3:25;

then A21: q . 1 = [((p . 1) `1),(chop ((dim2 ((p . 1),E)),w))] by A6

.= [x,(chop ((u ^ w),w))] by A1, A4

.= [x,u] by Def9 ;

len p in dom q by A5, A3, FINSEQ_3:25;

then q . (len q) = [((p . (len p)) `1),(chop ((dim2 ((p . (len p)),E)),w))] by A5, A6

.= [y,(chop ((v ^ w),w))] by A2, A20

.= [y,v] by Def9 ;

hence ex q being RedSequence of ==>.-relation TS st

( q . 1 = [x,u] & q . (len q) = [y,v] ) by A21; :: thesis: verum