:: by Micha{\l} Trybulec

::

:: Received May 5, 2009

:: Copyright (c) 2009-2019 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

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 )

ex q being FinSequence ex x being object st

( p = q ^ <*x*> & len p = (len q) + 1 )

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 )

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 )

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 )

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) ) )

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 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 )

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 )

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 )

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 )

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 ) )

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 c_{2} is strict ;

struct transition-system over X -> 1-sorted ;

aggr transition-system(# carrier, Tran #) -> transition-system over X;

sel Tran c_{2} -> Relation of [: the carrier of c_{2},X:], the carrier of c_{2};

end;
attr c

struct transition-system over X -> 1-sorted ;

aggr transition-system(# carrier, Tran #) -> transition-system over X;

sel Tran c

definition

let E be non empty set ;

let F be Subset of (E ^omega);

let TS be transition-system over F;

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

( 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 ) ) );

:: 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 ) ) ) );

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

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);

existence

ex b_{1} being transition-system over F st

( b_{1} is strict & not b_{1} is empty & b_{1} is finite & b_{1} is deterministic )

end;
let F be Subset of (E ^omega);

existence

ex b

( b

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

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 )

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 ;

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 :: 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

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 )

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 ;

end;
let F be Subset of (E ^omega);

let TS be transition-system over F;

let x1, x2, y1, y2 be object ;

:: 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 ) );

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 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

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

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 )

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 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

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 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

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

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

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 )

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;

ex b_{1} being Relation of [: the carrier of TS,(E ^omega):] st

for x1, x2, y1, y2 being object holds

( [[x1,x2],[y1,y2]] in b_{1} iff x1,x2 ==>. y1,y2,TS )

for b_{1}, b_{2} being Relation of [: the carrier of TS,(E ^omega):] st ( for x1, x2, y1, y2 being object holds

( [[x1,x2],[y1,y2]] in b_{1} iff x1,x2 ==>. y1,y2,TS ) ) & ( for x1, x2, y1, y2 being object holds

( [[x1,x2],[y1,y2]] in b_{2} iff x1,x2 ==>. y1,y2,TS ) ) holds

b_{1} = b_{2}

end;
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 for x1, x2, y1, y2 being object holds

( [[x1,x2],[y1,y2]] in it iff x1,x2 ==>. y1,y2,TS );

ex b

for x1, x2, y1, y2 being object holds

( [[x1,x2],[y1,y2]] in b

proof end;

uniqueness for b

( [[x1,x2],[y1,y2]] in b

( [[x1,x2],[y1,y2]] in b

b

proof 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 b_{4} being Relation of [: the carrier of TS,(E ^omega):] holds

( b_{4} = ==>.-relation TS iff for x1, x2, y1, y2 being object holds

( [[x1,x2],[y1,y2]] in b_{4} iff x1,x2 ==>. y1,y2,TS ) );

for E being non empty set

for F being Subset of (E ^omega)

for TS being non empty transition-system over F

for b

( b

( [[x1,x2],[y1,y2]] in b

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] )

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 )

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]]

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

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 )

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 )

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 )

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 )

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

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

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

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

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

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

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 )

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

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 ;

( ( 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 ) )

for b_{1} being Element of E ^omega holds verum
;

end;
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 x `2 if ex y being object ex u being Element of E ^omega st x = [y,u]

otherwise {} ;

( ( 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 b

:: 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) = {} ) );

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] )

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)] )

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 )

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

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

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

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

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

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 )

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 )

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 )

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 )

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

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 )

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

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

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

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 )

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

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

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

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

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

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

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)]

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)]

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]

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]

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

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

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 ) )

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

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

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

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 ;

end;
let F be Subset of (E ^omega);

let TS be non empty transition-system over F;

let x1, x2, y1, y2 be object ;

:: 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] );

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;

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;

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 :: REWRITE3:85

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

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

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 )

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

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;

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 ;

end;
let F be Subset of (E ^omega);

let TS be non empty transition-system over F;

let x1, x2, y be object ;

:: 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 );

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;

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 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

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

theorem :: REWRITE3:98

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

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 :: REWRITE3:101

theorem :: REWRITE3:102

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 ;

{ 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

end;
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 ) } ;

{ 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;

:: 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 ) } ;

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 ) )

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

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)

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;

:: Deterministic Transition Systems