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 :
theorem Th14:
begin
:: deftheorem Def2 defines -->. REWRITE3:def 2 :
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
begin
:: deftheorem Def3 defines ==>. REWRITE3:def 3 :
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 :
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 :
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 :
theorem Th94:
theorem Th95:
theorem Th96:
theorem
theorem
theorem
theorem Th100:
theorem
theorem
begin
:: deftheorem defines -succ_of REWRITE3:def 8 :
theorem Th103:
theorem
theorem