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


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

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

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

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

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 & (len Q) + 1 = len P )
proof end;

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 & (len Q) + 1 = len P )
proof end;

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 & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) )
proof end;

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

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

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

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

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

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

definition
let X be set ;
attr c2 is strict ;
struct transition-system over X -> 1-sorted ;
aggr transition-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;
attr TS is deterministic means :Def1: :: REWRITE3:def 1
( the Tran of TS is Function & not <%> E in rng (dom the Tran of TS) & ( for s being Element of TS
for u, v being Element of E ^omega st u <> v & [s,u] in dom the Tran of TS & [s,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & 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 & not <%> E in rng (dom the Tran of TS) & ( for s being Element of TS
for u, v being Element of E ^omega st u <> v & [s,u] in dom the Tran of TS & [s,v] in dom the Tran of TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u ) ) ) );

theorem :: 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
proof end;

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 & not b1 is empty & b1 is finite & b1 is deterministic )
proof end;
end;

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

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

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

theorem :: REWRITE3:16
for x, y, z being object
for X1, X2 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 & x,y -->. z,TS1 holds
x,y -->. z,TS2 ;

theorem Th17: :: REWRITE3:17
for x, y, z1, z2 being object
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 & x,y -->. z1,TS & x,y -->. z2,TS holds
z1 = z2 by FUNCT_1:def 1;

theorem :: REWRITE3:18
for x, y being object
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
proof end;

theorem Th19: :: REWRITE3:19
for x, z1, z2 being object
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 & x,u -->. z1,TS & x,v -->. z2,TS holds
for w being Element of E ^omega holds
( not u ^ w = v & not v ^ w = u )
proof end;

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 object ;
pred x1,x2 ==>. y1,y2,TS means :: REWRITE3:def 3
 ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v );
end;

:: deftheorem 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 object holds
( x1,x2 ==>. y1,y2,TS iff ex v, w being Element of E ^omega st
( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) );

theorem Th20: :: REWRITE3:20
for x1, x2, y1, y2 being object
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 & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) by Th15;

theorem Th21: :: REWRITE3:21
for x1, x2, y1, y2 being object
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 & x1,x2 ==>. y1,y2,TS1 holds
x1,x2 ==>. y1,y2,TS2
proof end;

theorem :: REWRITE3:22
for x, y being object
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 & u = w ^ v ) ;

theorem Th23: :: REWRITE3:23
for x, y, z being object
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 )
proof end;

theorem Th24: :: REWRITE3:24
for x, y being object
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 ) by AFINSQ_1:28;

theorem Th25: :: REWRITE3:25
for x, y being object
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
proof end;

theorem Th26: :: REWRITE3:26
for x, y being object
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 by Th9;

theorem Th27: :: REWRITE3:27
for x1, x2, y1, y2, z being object
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 & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds
y1 = y2
proof end;

theorem Th28: :: REWRITE3:28
for x, y, z being object
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
proof end;

theorem Th29: :: REWRITE3:29
for x, y being object
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) & x,u ==>. y,v,TS holds
len u > len v
proof end;

theorem Th30: :: REWRITE3:30
for x1, x2, y1, y2, z1, z2 being object
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 & x1,x2 ==>. y2,z2,TS holds
( y1 = y2 & z1 = z2 )
proof end;

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 object 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 object holds
( [[x1,x2],[y1,y2]] in b1 iff x1,x2 ==>. y1,y2,TS )
proof end;
uniqueness
for b1, b2 being Relation of [: the carrier of TS,(E ^omega):] st ( for x1, x2, y1, y2 being object holds
( [[x1,x2],[y1,y2]] in b1 iff x1,x2 ==>. y1,y2,TS ) ) & ( for x1, x2, y1, y2 being object holds
( [[x1,x2],[y1,y2]] in b2 iff x1,x2 ==>. y1,y2,TS ) ) holds
b1 = b2
proof end;
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 object holds
( [[x1,x2],[y1,y2]] in b4 iff x1,x2 ==>. y1,y2,TS ) );

theorem Th31: :: REWRITE3:31
for x, y being object
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] & y = [t,w] )
proof end;

theorem Th32: :: REWRITE3:32
for x1, x2, y1, y2 being object
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 & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS )
proof end;

theorem Th33: :: REWRITE3:33
for x being object
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]]
proof end;

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
proof end;

theorem Th35: :: REWRITE3:35
for x1, x2, y1, y2 being object
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 & x1,w -->. y1,TS & x2 = w ^ v )
proof end;

theorem Th36: :: REWRITE3:36
for x, y being object
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 & u = w ^ v )
proof end;

theorem Th37: :: REWRITE3:37
for x, y, z being object
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 )
proof end;

theorem Th38: :: REWRITE3:38
for x, y being object
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 )
proof end;

theorem :: REWRITE3:39
for x, y being object
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
proof end;

theorem :: REWRITE3:40
for x, y being object
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
proof end;

theorem :: REWRITE3:41
for x, y1, y2, z being object
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 & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds
y1 = y2
proof end;

theorem :: REWRITE3:42
for x, y being object
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) & [[x,u],[y,v]] in ==>.-relation TS holds
len u > len v
proof end;

theorem Th43: :: REWRITE3:43
for x, y, z being object
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
proof end;

theorem Th44: :: REWRITE3:44
for x, y1, y2 being object
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 & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds
y1 = y2
proof end;

theorem :: REWRITE3:45
for x, y1, y2, z1, z2 being object
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 & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds
( y1 = y2 & z1 = z2 )
proof end;

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
proof end;

definition
let x be object ;
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 object ex u being Element of E ^omega st x = [y,u]
otherwise {} ;
coherence
( ( ex y being object ex u being Element of E ^omega st x = [y,u] implies x `2 is Element of E ^omega ) & ( ( for y being object
for u being Element of E ^omega holds not x = [y,u] ) implies {} is Element of E ^omega ) )
proof end;
consistency
for b1 being Element of E ^omega holds verum ;
end;

:: deftheorem Def5 defines dim2 REWRITE3:def 5 :
for x being object
for E being non empty set holds
( ( ex y being object ex u being Element of E ^omega st x = [y,u] implies dim2 (x,E) = x `2 ) & ( ( for y being object
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 & 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] & P . (k + 1) = [t,w] )
proof end;

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 & k + 1 in dom P holds
( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] )
proof end;

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 & k + 1 in dom P holds
( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS )
proof end;

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 & the Tran of TS1 = the Tran of TS2 holds
for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2
proof end;

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 object 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
proof end;

theorem Th52: :: REWRITE3:52
for y being object
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
proof end;

theorem Th53: :: REWRITE3:53
for x, y being object
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] & P . (len P) = [y,w] holds
ex u being Element of E ^omega st v = u ^ w
proof end;

theorem Th54: :: REWRITE3:54
for x, y being object
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] & P . (len P) = [y,u] holds
for k being Nat st k in dom P holds
(P . k) `2 = u
proof end;

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 & k + 1 in dom P holds
ex v, w being Element of E ^omega st
( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v )
proof end;

theorem :: REWRITE3:56
for x, y being object
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 & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds
ex w being Element of E ^omega st
( x,w -->. y,TS & u = w ^ v )
proof end;

theorem Th57: :: REWRITE3:57
for x, y, z being object
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 )
proof end;

theorem Th58: :: REWRITE3:58
for x, y being object
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 )
proof end;

theorem Th59: :: REWRITE3:59
for x, y being object
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] & P . (len P) = [y,w] holds
len v >= len w
proof end;

theorem Th60: :: REWRITE3:60
for x, y being object
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] & P . (len P) = [y,u] holds
( len P = 1 & x = y )
proof end;

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
proof end;

theorem Th62: :: REWRITE3:62
for x, y being object
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] & P . (len P) = [y,(<%> E)] holds
len P <= (len u) + 1
proof end;

theorem Th63: :: REWRITE3:63
for x, y being object
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%>] & P . (len P) = [y,(<%> E)] holds
len P = 2
proof end;

theorem Th64: :: REWRITE3:64
for x, y being object
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] & P . (len P) = [y,w] & not len v > len w holds
( len P = 1 & x = y & v = w )
proof end;

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 & k + 1 in dom P holds
(P . k) `2 <> (P . (k + 1)) `2
proof end;

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 & l in dom P & k < l holds
(P . k) `2 <> (P . l) `2
proof end;

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 & k in dom Q holds
P . k = Q . k
proof end;

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 & len P = len Q holds
P = Q
proof end;

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 & (P . (len P)) `2 = (Q . (len Q)) `2 holds
P = Q
proof end;

theorem Th70: :: REWRITE3:70
for x, y being object
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
proof end;

theorem Th71: :: REWRITE3:71
for x, y being object
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)]
proof end;

theorem Th72: :: REWRITE3:72
for x, y, z being object
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)]
proof end;

theorem Th73: :: REWRITE3:73
for x, y being object
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]
proof end;

theorem Th74: :: REWRITE3:74
for x1, x2, y1, y2 being object
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]
proof end;

theorem Th75: :: REWRITE3:75
for x, y being object
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
proof end;

theorem :: REWRITE3:76
for x, y being object
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,w],[y,(v ^ w)] holds
v = <%> E
proof end;

theorem Th77: :: REWRITE3:77
for x, y being object
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 & v = w ) )
proof end;

theorem :: REWRITE3:78
for x, y being object
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) & ==>.-relation TS reduces [x,u],[y,u] holds
x = y
proof end;

theorem Th79: :: REWRITE3:79
for x, y being object
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) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds
[[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS
proof end;

theorem Th80: :: REWRITE3:80
for x, y1, y2, z being object
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 & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds
y1 = y2
proof end;

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 object ;
pred x1,x2 ==>* y1,y2,TS means :: REWRITE3:def 6
 ==>.-relation TS reduces [x1,x2],[y1,y2];
end;

:: deftheorem 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 object holds
( x1,x2 ==>* y1,y2,TS iff ==>.-relation TS reduces [x1,x2],[y1,y2] );

theorem Th81: :: REWRITE3:81
for x1, x2, y1, y2 being object
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 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds
x1,x2 ==>* y1,y2,TS2 by Th34;

theorem Th82: :: REWRITE3:82
for x, y being object
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 by REWRITE1:12;

theorem Th83: :: REWRITE3:83
for x1, x2, y1, y2, z1, z2 being object
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 & y1,y2 ==>* z1,z2,TS holds
x1,x2 ==>* z1,z2,TS by REWRITE1:16;

theorem Th84: :: REWRITE3:84
for x, y, z being object
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 by Th72;

theorem :: REWRITE3:85
for x, y being object
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 by Th73;

theorem Th86: :: REWRITE3:86
for x, y being object
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 by Th71;

theorem Th87: :: REWRITE3:87
for x1, x2, y1, y2 being object
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 by Th74;

theorem Th88: :: REWRITE3:88
for x, y being object
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 by Th70;

theorem Th89: :: REWRITE3:89
for x, y being object
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
proof end;

theorem :: REWRITE3:90
for x, y being object
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,w ==>* y,v ^ w,TS holds
v = <%> E
proof end;

theorem Th91: :: REWRITE3:91
for x, y being object
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 )
proof end;

theorem Th92: :: REWRITE3:92
for x, y being object
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) & x,<%e%> ==>* y, <%> E,TS holds
x,<%e%> ==>. y, <%> E,TS
proof end;

theorem Th93: :: REWRITE3:93
for x1, x2, y1, y2, z being object
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 & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds
y1 = y2 by Th80;

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 object ;
pred x1,x2 ==>* y,TS means :: REWRITE3:def 7
x1,x2 ==>* y, <%> E,TS;
end;

:: deftheorem 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 object holds
( x1,x2 ==>* y,TS iff x1,x2 ==>* y, <%> E,TS );

theorem Th94: :: REWRITE3:94
for x, y, z being object
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 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds
x,y ==>* z,TS2 by Th81;

theorem Th95: :: REWRITE3:95
for x being object
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 by Th82;

theorem Th96: :: REWRITE3:96
for x, y being object
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
proof end;

theorem :: REWRITE3:97
for x, y, z being object
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 by Th84;

theorem :: REWRITE3:98
for x1, x2, y being object
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 by Th87;

theorem :: REWRITE3:99
for x, y, z being object
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 & y,v ==>* z,TS holds
x,u ^ v ==>* z,TS
proof end;

theorem Th100: :: REWRITE3:100
for x, y being object
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 ) by Th91;

theorem :: REWRITE3:101
for x, y being object
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) & x,<%e%> ==>* y,TS holds
x,<%e%> ==>. y, <%> E,TS by Th92;

theorem :: REWRITE3:102
for x1, x2, y1, y2 being object
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 & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS holds
y1 = y2 by Th93;

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 be object ;
let X be set ;
func x -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 & t,x ==>* s,TS ) } ;
coherence
{ s where s is Element of TS : ex t being Element of TS st
( t in X & t,x ==>* s,TS ) } is Subset of TS
proof end;
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 being object
for 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 & t,x ==>* s,TS ) } ;

theorem Th103: :: REWRITE3:103
for x being object
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
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 & t,x ==>* s,TS ) )
proof end;

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
proof end;

theorem :: REWRITE3:105
for x being object
for 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 & the Tran of TS1 = the Tran of TS2 holds
x -succ_of (X,TS1) = x -succ_of (X,TS2)
proof end;