begin
theorem Th1:
theorem Th2:
theorem Th3:
begin
theorem Th4:
theorem Th5:
theorem
theorem
theorem Th8:
begin
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
begin
:: 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 of 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 Th14:
begin
:: deftheorem Def2 defines -->. REWRITE3:def 2 :
for X being set
for TS being transition-system of X
for x, y, z being set holds
( x,y -->. z,TS iff [[x,y],z] in the Tran of TS );
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
begin
:: deftheorem Def3 defines ==>. REWRITE3:def 3 :
for E being non empty set
for F being Subset of (E ^omega)
for TS being transition-system of 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 & x1,w -->. y1,TS & x2 = w ^ v ) );
theorem Th20:
theorem Th21:
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 of
F1 for
TS2 being
transition-system of
F2 st the
Tran of
TS1 = the
Tran of
TS2 &
x1,
x2 ==>. y1,
y2,
TS1 holds
x1,
x2 ==>. y1,
y2,
TS2
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
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 of
F st the
Tran of
TS is
Function &
x1,
x2 ==>. y1,
z,
TS &
x1,
x2 ==>. y2,
z,
TS holds
y1 = y2
theorem Th28:
theorem Th29:
theorem Th30:
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 of
F st
x1,
x2 ==>. y1,
z1,
TS &
x1,
x2 ==>. y2,
z2,
TS holds
(
y1 = y2 &
z1 = z2 )
begin
definition
let E be non
empty set ;
let F be
Subset of
(E ^omega);
let TS be non
empty transition-system of
F;
func ==>.-relation TS -> Relation of
[: the carrier of TS,(E ^omega):] means :
Def4:
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 )
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 ) ) & ( for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in b2 iff x1,x2 ==>. y1,y2,TS ) ) holds
b1 = b2
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 of 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:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem
theorem
theorem
theorem Th43:
theorem Th44:
theorem
theorem
begin
:: 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 ) & ( ( for y being set
for u being Element of E ^omega holds not x = [y,u] ) implies dim2 (x,E) = {} ) );
theorem Th47:
theorem Th48:
theorem Th49:
theorem
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem
theorem
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
begin
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem
theorem Th77:
theorem
theorem Th79:
theorem Th80:
begin
:: 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 of F
for x1, x2, y1, y2 being set holds
( x1,x2 ==>* y1,y2,TS iff ==>.-relation TS reduces [x1,x2],[y1,y2] );
theorem Th81:
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 of
F1 for
TS2 being non
empty transition-system of
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
theorem Th82:
theorem Th83:
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 of
F st
x1,
x2 ==>* y1,
y2,
TS &
y1,
y2 ==>* z1,
z2,
TS holds
x1,
x2 ==>* z1,
z2,
TS
theorem Th84:
theorem
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem
theorem Th91:
theorem Th92:
theorem Th93:
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 of
F st
TS is
deterministic &
x1,
x2 ==>* y1,
z,
TS &
x1,
x2 ==>* y2,
z,
TS holds
y1 = y2
begin
:: 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 of F
for x1, x2, y being set holds
( x1,x2 ==>* y,TS iff x1,x2 ==>* y, <%> E,TS );
theorem Th94:
theorem Th95:
theorem Th96:
theorem
theorem
theorem
theorem Th100:
theorem
theorem
begin
:: 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 of 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 & t,x ==>* s,TS ) } ;
theorem Th103:
theorem
theorem