:: Labelled State Transition Systems
:: by Micha{\l} Trybulec
::
:: Received May 5, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

theorem Th1: :: REWRITE3:1
for x being set
for k being Nat
for p being FinSequence st k in dom p holds
(<*x*> ^ p) . (k + 1) = p . k
proofend;

theorem Th2: :: REWRITE3:2
for p being FinSequence st p <> {} holds
ex q being FinSequence ex x being set st
( p = q ^ <*x*> &amp; len p = (len q) + 1 )
proofend;

theorem Th3: :: REWRITE3:3
for k being Nat
for p being FinSequence st k in dom p &amp; not k + 1 in dom p holds
len p = k
proofend;

begin

theorem Th4: :: REWRITE3:4
for R being Relation
for P being RedSequence of R
for q1, q2 being FinSequence st P = q1 ^ q2 &amp; len q1 > 0 &amp; len q2 > 0 holds
( q1 is RedSequence of R &amp; q2 is RedSequence of R )
proofend;

theorem Th5: :: REWRITE3:5
for R being Relation
for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P &amp; (len Q) + 1 = len P )
proofend;

theorem :: REWRITE3:6
for R being Relation
for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( Q ^ <*(P . (len P))*> = P &amp; (len Q) + 1 = len P )
proofend;

theorem :: REWRITE3:7
for R being Relation
for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( (len Q) + 1 = len P &amp; ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) )
proofend;

theorem Th8: :: REWRITE3:8
for x, y being set
for R being Relation st <*x,y*> is RedSequence of R holds
[x,y] in R
proofend;

begin

theorem Th9: :: REWRITE3:9
for E being non empty set
for w, u, v being Element of E ^omega st w = u ^ v holds
( len u <= len w &amp; len v <= len w )
proofend;

theorem Th10: :: REWRITE3:10
for E being non empty set
for w, u, v being Element of E ^omega st w = u ^ v &amp; u <> <%> E &amp; v <> <%> E holds
( len u < len w &amp; len v < len w )
proofend;

theorem :: REWRITE3:11
for E being non empty set
for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 &amp; ( len w1 = len w2 or len v1 = len v2 ) holds
( w1 = w2 &amp; v1 = v2 )
proofend;

theorem Th12: :: REWRITE3:12
for E being non empty set
for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 &amp; ( len w1 <= len w2 or len v1 >= len v2 ) holds
ex u being Element of E ^omega st
( w1 ^ u = w2 &amp; v1 = u ^ v2 )
proofend;

theorem Th13: :: REWRITE3:13
for E being non empty set
for w1, v1, w2, v2 being Element of E ^omega holds
( not w1 ^ v1 = w2 ^ v2 or ex u being Element of E ^omega st
( w1 ^ u = w2 &amp; v1 = u ^ v2 ) or ex u being Element of E ^omega st
( w2 ^ u = w1 &amp; v2 = u ^ v1 ) )
proofend;

begin

definition
let X be set ;
attrc2 is strict ;
struct transition-system over X ->  1-sorted ;
aggrtransition-system(# carrier, Tran #) ->  transition-system over X;
sel Tran c2 ->  Relation of [: the carrier of c2,X:], the carrier of c2;
end;

:: Transition Systems over Subsets of E^omega
:: Deterministic Transition Systems
definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be transition-system over F;
attrTS is deterministic  means :Def1: :: REWRITE3:def 1
( the Tran of TS is Function &amp; not <%> E in rng (dom the Tran of TS) &amp; ( for s being Element of TS
for u, v being Element of E ^omega st u <> v &amp; [s,u] in dom the Tran of TS &amp; [s,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v &amp; not v ^ w = u ) ) );
end;

:: deftheorem Def1 defines deterministic REWRITE3:def_1_:_
 for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( TS is deterministic iff ( the Tran of TS is Function &amp; not <%> E in rng (dom the Tran of TS) &amp; ( for s being Element of TS
for u, v being Element of E ^omega st u <> v &amp; [s,u] in dom the Tran of TS &amp; [s,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v &amp; not v ^ w = u ) ) ) );

theorem Th14: :: REWRITE3:14
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st dom the Tran of TS = {} holds
TS is deterministic
proofend;

registration
let E be non empty set ;
let F be Subset of (E ^omega);
cluster non empty finite strict deterministic for transition-system over F;
existence
 ex b1 being transition-system over F st
( b1 is strict &amp; not b1 is empty &amp; b1 is finite &amp; b1 is deterministic )
proofend;
end;

begin

definition
let X be set ;
let TS be transition-system over X;
let x, y, z be set ;
predx,y -->. z,TS means :Def2: :: REWRITE3:def 2
[[x,y],z] in the Tran of TS;
end;

:: deftheorem Def2 defines -->. REWRITE3:def_2_:_
 for X being set
for TS being transition-system over X
for x, y, z being set holds
( x,y -->. z,TS iff [[x,y],z] in the Tran of TS );

theorem Th15: :: REWRITE3:15
for X, x, y, z being set
for TS being transition-system over X st x,y -->. z,TS holds
( x in TS &amp; y in X &amp; z in TS &amp; x in dom (dom the Tran of TS) &amp; y in rng (dom the Tran of TS) &amp; z in rng the Tran of TS )
proofend;

theorem Th16: :: REWRITE3:16
for X1, X2, x, y, z being set
for TS1 being transition-system over X1
for TS2 being transition-system over X2 st the Tran of TS1 = the Tran of TS2 &amp; x,y -->. z,TS1 holds
x,y -->. z,TS2
proofend;

theorem Th17: :: REWRITE3:17
for x, y, z1, z2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function &amp; x,y -->. z1,TS &amp; x,y -->. z2,TS holds
z1 = z2
proofend;

theorem :: REWRITE3:18
for x, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x, <%> E -->. y,TS
proofend;

theorem Th19: :: REWRITE3:19
for x, z1, z2 being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st u <> v &amp; x,u -->. z1,TS &amp; x,v -->. z2,TS holds
for w being Element of E ^omega holds
( not u ^ w = v &amp; not v ^ w = u )
proofend;

begin

definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be transition-system over F;
let x1, x2, y1, y2 be set ;
predx1,x2 ==>. y1,y2,TS means :Def3: :: REWRITE3:def 3
 ex v, w being Element of E ^omega st
( v = y2 &amp; x1,w -->. y1,TS &amp; x2 = w ^ v );
end;

:: deftheorem Def3 defines ==>. REWRITE3:def_3_:_
 for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F
for x1, x2, y1, y2 being set holds
( x1,x2 ==>. y1,y2,TS iff ex v, w being Element of E ^omega st
( v = y2 &amp; x1,w -->. y1,TS &amp; x2 = w ^ v ) );

theorem Th20: :: REWRITE3:20
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st x1,x2 ==>. y1,y2,TS holds
( x1 in TS &amp; y1 in TS &amp; x2 in E ^omega &amp; y2 in E ^omega &amp; x1 in dom (dom the Tran of TS) &amp; y1 in rng the Tran of TS )
proofend;

theorem Th21: :: REWRITE3:21
for x1, x2, y1, y2 being set
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being transition-system over F1
for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 &amp; x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
proofend;

theorem Th22: :: REWRITE3:22
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS &amp; u = w ^ v )
proofend;

theorem Th23: :: REWRITE3:23
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( x,y -->. z,TS iff x,y ==>. z, <%> E,TS )
proofend;

theorem Th24: :: REWRITE3:24
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F holds
( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS )
proofend;

theorem Th25: :: REWRITE3:25
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
x,u ^ w ==>. y,v ^ w,TS
proofend;

theorem Th26: :: REWRITE3:26
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st x,u ==>. y,v,TS holds
len u >= len v
proofend;

theorem Th27: :: REWRITE3:27
for x1, x2, y1, z, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st the Tran of TS is Function &amp; x1,x2 ==>. y1,z,TS &amp; x1,x2 ==>. y2,z,TS holds
y1 = y2
proofend;

theorem Th28: :: REWRITE3:28
for x, z, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not x,z ==>. y,z,TS
proofend;

theorem Th29: :: REWRITE3:29
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) &amp; x,u ==>. y,v,TS holds
len u > len v
proofend;

theorem Th30: :: REWRITE3:30
for x1, x2, y1, z1, y2, z2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS &amp; x1,x2 ==>. y2,z2,TS holds
( y1 = y2 &amp; z1 = z2 )
proofend;

begin

definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be non empty transition-system over F;
func ==>.-relation TS ->  Relation of [: the carrier of TS,(E ^omega):] means :Def4: :: REWRITE3:def 4
 for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in it iff x1,x2 ==>. y1,y2,TS );
existence
 ex b1 being Relation of [: the carrier of TS,(E ^omega):] st
for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in b1 iff x1,x2 ==>. y1,y2,TS )
proofend;
uniqueness
 for b1, b2 being Relation of [: the carrier of TS,(E ^omega):] st ( for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in b1 iff x1,x2 ==>. y1,y2,TS ) ) &amp; ( for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in b2 iff x1,x2 ==>. y1,y2,TS ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines ==>.-relation REWRITE3:def_4_:_
 for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for b4 being Relation of [: the carrier of TS,(E ^omega):] holds
( b4 = ==>.-relation TS iff for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in b4 iff x1,x2 ==>. y1,y2,TS ) );

theorem Th31: :: REWRITE3:31
for x, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [x,y] in ==>.-relation TS holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( x = [s,v] &amp; y = [t,w] )
proofend;

theorem Th32: :: REWRITE3:32
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds
( x1 in TS &amp; y1 in TS &amp; x2 in E ^omega &amp; y2 in E ^omega &amp; x1 in dom (dom the Tran of TS) &amp; y1 in rng the Tran of TS )
proofend;

theorem Th33: :: REWRITE3:33
for x being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x in ==>.-relation TS holds
ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]]
proofend;

theorem Th34: :: REWRITE3:34
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds
==>.-relation TS1 = ==>.-relation TS2
proofend;

theorem Th35: :: REWRITE3:35
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds
ex v, w being Element of E ^omega st
( v = y2 &amp; x1,w -->. y1,TS &amp; x2 = w ^ v )
proofend;

theorem Th36: :: REWRITE3:36
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
ex w being Element of E ^omega st
( x,w -->. y,TS &amp; u = w ^ v )
proofend;

theorem Th37: :: REWRITE3:37
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS )
proofend;

theorem Th38: :: REWRITE3:38
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS )
proofend;

theorem :: REWRITE3:39
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
[[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS
proofend;

theorem :: REWRITE3:40
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds
len u >= len v
proofend;

theorem :: REWRITE3:41
for x, y1, z, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st the Tran of TS is Function &amp; [x,[y1,z]] in ==>.-relation TS &amp; [x,[y2,z]] in ==>.-relation TS holds
y1 = y2
proofend;

theorem :: REWRITE3:42
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) &amp; [[x,u],[y,v]] in ==>.-relation TS holds
len u > len v
proofend;

theorem Th43: :: REWRITE3:43
for x, z, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
not [[x,z],[y,z]] in ==>.-relation TS
proofend;

theorem Th44: :: REWRITE3:44
for x, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic &amp; [x,y1] in ==>.-relation TS &amp; [x,y2] in ==>.-relation TS holds
y1 = y2
proofend;

theorem :: REWRITE3:45
for x, y1, z1, y2, z2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic &amp; [x,[y1,z1]] in ==>.-relation TS &amp; [x,[y2,z2]] in ==>.-relation TS holds
( y1 = y2 &amp; z1 = z2 )
proofend;

theorem :: REWRITE3:46
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
==>.-relation TS is Function-like
proofend;

begin

definition
let x be set ;
let E be non empty set ;
func dim2 (x,E) ->  Element of E ^omega  equals :Def5: :: REWRITE3:def 5
x `2  if  ex y being set ex u being Element of E ^omega st x = [y,u]
otherwise  {} ;
coherence
 ( ( ex y being set ex u being Element of E ^omega st x = [y,u] implies x `2 is Element of E ^omega ) &amp; ( ( for y being set
for u being Element of E ^omega holds not x = [y,u] ) implies {} is Element of E ^omega ) )
proofend;
consistency
 for b1 being Element of E ^omega holds verum ;
end;

:: deftheorem Def5 defines dim2 REWRITE3:def_5_:_
 for x being set
for E being non empty set holds
( ( ex y being set ex u being Element of E ^omega st x = [y,u] implies dim2 (x,E) = x `2 ) &amp; ( ( for y being set
for u being Element of E ^omega holds not x = [y,u] ) implies dim2 (x,E) = {} ) );

theorem Th47: :: REWRITE3:47
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P &amp; k + 1 in dom P holds
ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st
( P . k = [s,v] &amp; P . (k + 1) = [t,w] )
proofend;

theorem Th48: :: REWRITE3:48
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P &amp; k + 1 in dom P holds
( P . k = [((P . k) `1),((P . k) `2)] &amp; P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] )
proofend;

theorem Th49: :: REWRITE3:49
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P &amp; k + 1 in dom P holds
( (P . k) `1 in TS &amp; (P . k) `2 in E ^omega &amp; (P . (k + 1)) `1 in TS &amp; (P . (k + 1)) `2 in E ^omega &amp; (P . k) `1 in dom (dom the Tran of TS) &amp; (P . (k + 1)) `1 in rng the Tran of TS )
proofend;

theorem :: REWRITE3:50
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 &amp; the Tran of TS1 = the Tran of TS2 holds
for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
proofend;

theorem Th51: :: REWRITE3:51
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds
for k being Nat st k in dom P holds
dim2 ((P . k),E) = (P . k) `2
proofend;

theorem Th52: :: REWRITE3:52
for y being set
for E being non empty set
for w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds
for k being Nat st k in dom P holds
ex u being Element of E ^omega st (P . k) `2 = u ^ w
proofend;

theorem Th53: :: REWRITE3:53
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] &amp; P . (len P) = [y,w] holds
ex u being Element of E ^omega st v = u ^ w
proofend;

theorem Th54: :: REWRITE3:54
for x, y being set
for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] &amp; P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
proofend;

theorem :: REWRITE3:55
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P &amp; k + 1 in dom P holds
ex v, w being Element of E ^omega st
( v = (P . (k + 1)) `2 &amp; (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS &amp; (P . k) `2 = w ^ v )
proofend;

theorem :: REWRITE3:56
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P &amp; k + 1 in dom P &amp; P . k = [x,u] &amp; P . (k + 1) = [y,v] holds
ex w being Element of E ^omega st
( x,w -->. y,TS &amp; u = w ^ v )
proofend;

theorem Th57: :: REWRITE3:57
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS )
proofend;

theorem Th58: :: REWRITE3:58
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS )
proofend;

theorem Th59: :: REWRITE3:59
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] &amp; P . (len P) = [y,w] holds
len v >= len w
proofend;

theorem Th60: :: REWRITE3:60
for x, y being set
for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] &amp; P . (len P) = [y,u] holds
( len P = 1 &amp; x = y )
proofend;

theorem Th61: :: REWRITE3:61
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds
len P = 1
proofend;

theorem Th62: :: REWRITE3:62
for x, y being set
for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] &amp; P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
proofend;

theorem Th63: :: REWRITE3:63
for x, y being set
for E being non empty set
for e being Element of E
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] &amp; P . (len P) = [y,(<%> E)] holds
len P = 2
proofend;

theorem Th64: :: REWRITE3:64
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] &amp; P . (len P) = [y,w] &amp; not len v > len w holds
( len P = 1 &amp; x = y &amp; v = w )
proofend;

theorem :: REWRITE3:65
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS
for k being Nat st k in dom P &amp; k + 1 in dom P holds
(P . k) `2 <> (P . (k + 1)) `2
proofend;

theorem Th66: :: REWRITE3:66
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
for P being RedSequence of ==>.-relation TS
for k, l being Nat st k in dom P &amp; l in dom P &amp; k < l holds
(P . k) `2 <> (P . l) `2
proofend;

theorem Th67: :: REWRITE3:67
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds
for k being Nat st k in dom P &amp; k in dom Q holds
P . k = Q . k
proofend;

theorem Th68: :: REWRITE3:68
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 &amp; len P = len Q holds
P = Q
proofend;

theorem Th69: :: REWRITE3:69
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic holds
for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 &amp; (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q
proofend;

begin

theorem Th70: :: REWRITE3:70
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
ex u being Element of E ^omega st v = u ^ w
proofend;

theorem Th71: :: REWRITE3:71
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds
==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)]
proofend;

theorem Th72: :: REWRITE3:72
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
==>.-relation TS reduces [x,y],[z,(<%> E)]
proofend;

theorem Th73: :: REWRITE3:73
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v -->. y,TS holds
==>.-relation TS reduces [x,(v ^ w)],[y,w]
proofend;

theorem Th74: :: REWRITE3:74
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
==>.-relation TS reduces [x1,x2],[y1,y2]
proofend;

theorem Th75: :: REWRITE3:75
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds
len v >= len w
proofend;

theorem :: REWRITE3:76
for x, y being set
for E being non empty set
for w, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds
v = <%> E
proofend;

theorem Th77: :: REWRITE3:77
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds
( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y &amp; v = w ) )
proofend;

theorem :: REWRITE3:78
for x, y being set
for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) &amp; ==>.-relation TS reduces [x,u],[y,u] holds
x = y
proofend;

theorem Th79: :: REWRITE3:79
for x, y being set
for E being non empty set
for e being Element of E
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) &amp; ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds
[[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS
proofend;

theorem Th80: :: REWRITE3:80
for x, y1, z, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic &amp; ==>.-relation TS reduces x,[y1,z] &amp; ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
proofend;

begin

definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be non empty transition-system over F;
let x1, x2, y1, y2 be set ;
predx1,x2 ==>* y1,y2,TS means :Def6: :: REWRITE3:def 6
 ==>.-relation TS reduces [x1,x2],[y1,y2];
end;

:: deftheorem Def6 defines ==>* REWRITE3:def_6_:_
 for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for x1, x2, y1, y2 being set holds
( x1,x2 ==>* y1,y2,TS iff ==>.-relation TS reduces [x1,x2],[y1,y2] );

theorem Th81: :: REWRITE3:81
for x1, x2, y1, y2 being set
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 &amp; the Tran of TS1 = the Tran of TS2 &amp; x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,TS2
proofend;

theorem Th82: :: REWRITE3:82
for x, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds x,y ==>* x,y,TS
proofend;

theorem Th83: :: REWRITE3:83
for x1, x2, y1, y2, z1, z2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>* y1,y2,TS &amp; y1,y2 ==>* z1,z2,TS holds
x1,x2 ==>* z1,z2,TS
proofend;

theorem Th84: :: REWRITE3:84
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z, <%> E,TS
proofend;

theorem :: REWRITE3:85
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v -->. y,TS holds
x,v ^ w ==>* y,w,TS
proofend;

theorem Th86: :: REWRITE3:86
for x, y being set
for E being non empty set
for u, v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,v,TS holds
x,u ^ w ==>* y,v ^ w,TS
proofend;

theorem Th87: :: REWRITE3:87
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds
x1,x2 ==>* y1,y2,TS
proofend;

theorem Th88: :: REWRITE3:88
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
ex u being Element of E ^omega st v = u ^ w
proofend;

theorem Th89: :: REWRITE3:89
for x, y being set
for E being non empty set
for v, w being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,v ==>* y,w,TS holds
len w <= len v
proofend;

theorem :: REWRITE3:90
for x, y being set
for E being non empty set
for w, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds
v = <%> E
proofend;

theorem Th91: :: REWRITE3:91
for x, y being set
for E being non empty set
for u being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x,u ==>* y,u,TS iff x = y )
proofend;

theorem Th92: :: REWRITE3:92
for x, y being set
for E being non empty set
for e being Element of E
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) &amp; x,<%e%> ==>* y, <%> E,TS holds
x,<%e%> ==>. y, <%> E,TS
proofend;

theorem Th93: :: REWRITE3:93
for x1, x2, y1, z, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic &amp; x1,x2 ==>* y1,z,TS &amp; x1,x2 ==>* y2,z,TS holds
y1 = y2
proofend;

begin

definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be non empty transition-system over F;
let x1, x2, y be set ;
predx1,x2 ==>* y,TS means :Def7: :: REWRITE3:def 7
x1,x2 ==>* y, <%> E,TS;
end;

:: deftheorem Def7 defines ==>* REWRITE3:def_7_:_
 for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for x1, x2, y being set holds
( x1,x2 ==>* y,TS iff x1,x2 ==>* y, <%> E,TS );

theorem Th94: :: REWRITE3:94
for x, y, z being set
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 &amp; the Tran of TS1 = the Tran of TS2 &amp; x,y ==>* z,TS1 holds
x,y ==>* z,TS2
proofend;

theorem Th95: :: REWRITE3:95
for x being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F holds x, <%> E ==>* x,TS
proofend;

theorem Th96: :: REWRITE3:96
for x, y being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,TS holds
x,u ^ v ==>* y,v,TS
proofend;

theorem :: REWRITE3:97
for x, y, z being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,y -->. z,TS holds
x,y ==>* z,TS
proofend;

theorem :: REWRITE3:98
for x1, x2, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x1,x2 ==>. y, <%> E,TS holds
x1,x2 ==>* y,TS
proofend;

theorem :: REWRITE3:99
for x, y, z being set
for E being non empty set
for u, v being Element of E ^omega
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st x,u ==>* y,TS &amp; y,v ==>* z,TS holds
x,u ^ v ==>* z,TS
proofend;

theorem Th100: :: REWRITE3:100
for x, y being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds
( x, <%> E ==>* y,TS iff x = y )
proofend;

theorem :: REWRITE3:101
for x, y being set
for E being non empty set
for e being Element of E
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) &amp; x,<%e%> ==>* y,TS holds
x,<%e%> ==>. y, <%> E,TS
proofend;

theorem :: REWRITE3:102
for x1, x2, y1, y2 being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F st TS is deterministic &amp; x1,x2 ==>* y1,TS &amp; x1,x2 ==>* y2,TS holds
y1 = y2
proofend;

begin

definition
let E be non empty set ;
let F be Subset of (E ^omega);
let TS be non empty transition-system over F;
let x, X be set ;
funcx -succ_of (X,TS) ->  Subset of TS equals :: REWRITE3:def 8
 {  s where s is Element of TS : ex t being Element of TS st
( t in X &amp; t,x ==>* s,TS )  }  ;
coherence
  {  s where s is Element of TS : ex t being Element of TS st
( t in X &amp; t,x ==>* s,TS )  }  is Subset of TS
proofend;
end;

:: deftheorem  defines -succ_of REWRITE3:def_8_:_
 for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for x, X being set holds x -succ_of (X,TS) =  {  s where s is Element of TS : ex t being Element of TS st
( t in X &amp; t,x ==>* s,TS )  }  ;

theorem Th103: :: REWRITE3:103
for x, X being set
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for s being Element of TS holds
( s in x -succ_of (X,TS) iff ex t being Element of TS st
( t in X &amp; t,x ==>* s,TS ) )
proofend;

theorem :: REWRITE3:104
for E being non empty set
for F being Subset of (E ^omega)
for TS being non empty transition-system over F
for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds
(<%> E) -succ_of (S,TS) = S
proofend;

theorem :: REWRITE3:105
for x, X being set
for E being non empty set
for F1, F2 being Subset of (E ^omega)
for TS1 being non empty transition-system over F1
for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 &amp; the Tran of TS1 = the Tran of TS2 holds
x -succ_of (X,TS1) = x -succ_of (X,TS2)
proofend;