:: Labelled State Transition Systems
:: by Micha{\l} Trybulec
::
:: Received May 5, 2009
:: Copyright (c) 2009 Association of Mizar Users
theorem Th1: :: REWRITE3:1
theorem Th2: :: REWRITE3:2
theorem Th3: :: REWRITE3:3
theorem Th4: :: REWRITE3:4
theorem Th5: :: REWRITE3:5
theorem :: REWRITE3:6
theorem :: REWRITE3:7
theorem Th8: :: REWRITE3:8
theorem Th9: :: REWRITE3:9
theorem Th10: :: REWRITE3:10
theorem :: REWRITE3:11
theorem Th12: :: REWRITE3:12
theorem Th13: :: REWRITE3:13
:: deftheorem Def1 defines deterministic REWRITE3:def 1 :
theorem Th14: :: REWRITE3:14
:: deftheorem Def2 defines -->. REWRITE3:def 2 :
theorem Th15: :: REWRITE3:15
theorem Th16: :: REWRITE3:16
theorem Th17: :: REWRITE3:17
theorem :: REWRITE3:18
theorem Th19: :: REWRITE3:19
:: deftheorem Def3 defines ==>. REWRITE3:def 3 :
theorem Th20: :: REWRITE3:20
theorem Th21: :: REWRITE3:21
for
x1,
x2,
y1,
y2 being
set for
E being non
empty set for
F1,
F2 being
Subset of
(E ^omega ) for
TS1 being
transition-system 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: :: REWRITE3:22
theorem Th23: :: REWRITE3:23
theorem Th24: :: REWRITE3:24
theorem Th25: :: REWRITE3:25
theorem Th26: :: REWRITE3:26
theorem Th27: :: REWRITE3:27
for
x1,
x2,
y1,
z,
y2 being
set for
E being non
empty set for
F being
Subset of
(E ^omega ) for
TS being
transition-system of
F st the
Tran of
TS is
Function &
x1,
x2 ==>. y1,
z,
TS &
x1,
x2 ==>. y2,
z,
TS holds
y1 = y2
theorem Th28: :: REWRITE3:28
theorem Th29: :: REWRITE3:29
theorem Th30: :: REWRITE3:30
for
x1,
x2,
y1,
z1,
y2,
z2 being
set for
E being non
empty set for
F being
Subset of
(E ^omega ) for
TS being
deterministic transition-system of
F st
x1,
x2 ==>. y1,
z1,
TS &
x1,
x2 ==>. y2,
z2,
TS holds
(
y1 = y2 &
z1 = z2 )
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:
:: REWRITE3:def 4
for
x1,
x2,
y1,
y2 being
set holds
(
[[x1,x2],[y1,y2]] in it iff
x1,
x2 ==>. y1,
y2,
TS );
existence
ex b1 being Relation of [:the carrier of TS,(E ^omega ):] st
for x1, x2, y1, y2 being set holds
( [[x1,x2],[y1,y2]] in b1 iff x1,x2 ==>. y1,y2,TS )
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: :: REWRITE3:31
theorem Th32: :: REWRITE3:32
theorem Th33: :: REWRITE3:33
theorem Th34: :: REWRITE3:34
theorem Th35: :: REWRITE3:35
theorem Th36: :: REWRITE3:36
theorem Th37: :: REWRITE3:37
theorem Th38: :: REWRITE3:38
theorem :: REWRITE3:39
theorem :: REWRITE3:40
theorem :: REWRITE3:41
theorem :: REWRITE3:42
theorem Th43: :: REWRITE3:43
theorem Th44: :: REWRITE3:44
theorem :: REWRITE3:45
theorem :: REWRITE3:46
:: deftheorem Def5 defines dim2 REWRITE3:def 5 :
theorem Th47: :: REWRITE3:47
theorem Th48: :: REWRITE3:48
theorem Th49: :: REWRITE3:49
theorem :: REWRITE3:50
theorem Th51: :: REWRITE3:51
theorem Th52: :: REWRITE3:52
theorem Th53: :: REWRITE3:53
theorem Th54: :: REWRITE3:54
theorem :: REWRITE3:55
theorem :: REWRITE3:56
theorem Th57: :: REWRITE3:57
theorem Th58: :: REWRITE3:58
theorem Th59: :: REWRITE3:59
theorem Th60: :: REWRITE3:60
theorem Th61: :: REWRITE3:61
theorem Th62: :: REWRITE3:62
theorem Th63: :: REWRITE3:63
theorem Th64: :: REWRITE3:64
theorem :: REWRITE3:65
theorem Th66: :: REWRITE3:66
theorem Th67: :: REWRITE3:67
theorem Th68: :: REWRITE3:68
theorem Th69: :: REWRITE3:69
theorem Th70: :: REWRITE3:70
theorem Th71: :: REWRITE3:71
theorem Th72: :: REWRITE3:72
theorem Th73: :: REWRITE3:73
theorem Th74: :: REWRITE3:74
theorem Th75: :: REWRITE3:75
theorem :: REWRITE3:76
theorem Th77: :: REWRITE3:77
theorem :: REWRITE3:78
theorem Th79: :: REWRITE3:79
theorem Th80: :: REWRITE3:80
:: deftheorem Def6 defines ==>* REWRITE3:def 6 :
theorem Th81: :: REWRITE3:81
for
x1,
x2,
y1,
y2 being
set for
E being non
empty set for
F1,
F2 being
Subset of
(E ^omega ) for
TS1 being non
empty transition-system 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: :: REWRITE3:82
theorem Th83: :: REWRITE3:83
for
x1,
x2,
y1,
y2,
z1,
z2 being
set for
E being non
empty set for
F being
Subset of
(E ^omega ) for
TS being non
empty transition-system of
F st
x1,
x2 ==>* y1,
y2,
TS &
y1,
y2 ==>* z1,
z2,
TS holds
x1,
x2 ==>* z1,
z2,
TS
theorem Th84: :: REWRITE3:84
theorem :: REWRITE3:85
theorem Th86: :: REWRITE3:86
theorem Th87: :: REWRITE3:87
theorem Th88: :: REWRITE3:88
theorem Th89: :: REWRITE3:89
theorem :: REWRITE3:90
theorem Th91: :: REWRITE3:91
theorem Th92: :: REWRITE3:92
theorem Th93: :: REWRITE3:93
for
x1,
x2,
y1,
z,
y2 being
set for
E being non
empty set for
F being
Subset of
(E ^omega ) for
TS being non
empty transition-system of
F st
TS is
deterministic &
x1,
x2 ==>* y1,
z,
TS &
x1,
x2 ==>* y2,
z,
TS holds
y1 = y2
:: deftheorem Def7 defines ==>* REWRITE3:def 7 :
theorem Th94: :: REWRITE3:94
theorem Th95: :: REWRITE3:95
theorem Th96: :: REWRITE3:96
theorem :: REWRITE3:97
theorem :: REWRITE3:98
theorem :: REWRITE3:99
theorem Th100: :: REWRITE3:100
theorem :: REWRITE3:101
theorem :: REWRITE3:102
:: deftheorem defines -succ_of REWRITE3:def 8 :
theorem Th103: :: REWRITE3:103
theorem :: REWRITE3:104
theorem :: REWRITE3:105