:: Labelled State Transition Systems
:: by Micha{\l} Trybulec
::
:: Received May 5, 2009
:: Copyright (c) 2009 Association of Mizar Users
theorem LmSeq10: :: REWRITE3:1
theorem LmSeq20: :: REWRITE3:2
theorem LmSeq40: :: REWRITE3:3
theorem LmRed5: :: REWRITE3:4
theorem LmRed10: :: REWRITE3:5
theorem :: REWRITE3:6
theorem :: REWRITE3:7
theorem LmRed40: :: REWRITE3:8
theorem LmXSeq50: :: REWRITE3:9
theorem LmXSeq60: :: REWRITE3:10
theorem :: REWRITE3:11
theorem LmXSeq66: :: REWRITE3:12
theorem LmXSeq70: :: REWRITE3:13
:: deftheorem DefDetTS defines deterministic REWRITE3:def 1 :
theorem ThDet10: :: REWRITE3:14
:: deftheorem DefProd defines -->. REWRITE3:def 2 :
theorem ThProd30: :: REWRITE3:15
theorem ThProd40: :: REWRITE3:16
theorem ThProd50: :: REWRITE3:17
theorem :: REWRITE3:18
theorem ThProd70: :: REWRITE3:19
:: deftheorem DefDir defines ==>. REWRITE3:def 3 :
theorem ThDir10: :: REWRITE3:20
theorem ThDir15: :: 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 ThDir25: :: REWRITE3:22
theorem ThDir20: :: REWRITE3:23
theorem ThDir26: :: REWRITE3:24
theorem ThDir30: :: REWRITE3:25
theorem ThDir35: :: REWRITE3:26
theorem ThDir40: :: 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 ThDir60: :: REWRITE3:28
theorem ThDir50: :: REWRITE3:29
theorem ThDir70: :: 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 :
DefRel:
:: 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 DefRel 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 ThRel10: :: REWRITE3:31
theorem ThRel11: :: REWRITE3:32
theorem ThRel9: :: REWRITE3:33
theorem ThRel20: :: REWRITE3:34
theorem ThRel30: :: REWRITE3:35
theorem ThRel40: :: REWRITE3:36
theorem ThRel50: :: REWRITE3:37
theorem ThRel60: :: REWRITE3:38
theorem :: REWRITE3:39
theorem :: REWRITE3:40
theorem :: REWRITE3:41
theorem :: REWRITE3:42
theorem ThRel110: :: REWRITE3:43
theorem ThRel120': :: REWRITE3:44
theorem :: REWRITE3:45
theorem :: REWRITE3:46
:: deftheorem DefDim2 defines dim2 REWRITE3:def 5 :
theorem ThRedSeq4: :: REWRITE3:47
theorem ThRedSeq5: :: REWRITE3:48
theorem ThRedSeq10: :: REWRITE3:49
theorem :: REWRITE3:50
theorem ThRedSeq30: :: REWRITE3:51
theorem ThRedSeq50: :: REWRITE3:52
theorem ThRedSeq60: :: REWRITE3:53
theorem ThRedSeq70: :: REWRITE3:54
theorem :: REWRITE3:55
theorem :: REWRITE3:56
theorem ThRedSeq77: :: REWRITE3:57
theorem ThRedSeq78: :: REWRITE3:58
theorem ThRedSeq79: :: REWRITE3:59
theorem ThRedSeq80: :: REWRITE3:60
theorem ThRedSeq81: :: REWRITE3:61
theorem ThRedSeq90: :: REWRITE3:62
theorem ThRedSeq100: :: REWRITE3:63
theorem ThRedSeq110: :: REWRITE3:64
theorem :: REWRITE3:65
theorem ThRedSeq125: :: REWRITE3:66
theorem ThRedSeq130: :: REWRITE3:67
theorem ThRedSeq135: :: REWRITE3:68
theorem ThRedSeq140: :: REWRITE3:69
theorem ThRed60: :: REWRITE3:70
theorem ThRed70: :: REWRITE3:71
theorem ThRed81: :: REWRITE3:72
theorem ThRed82: :: REWRITE3:73
theorem ThRed83: :: REWRITE3:74
theorem ThRed84: :: REWRITE3:75
theorem :: REWRITE3:76
theorem ThRed110: :: REWRITE3:77
theorem :: REWRITE3:78
theorem ThRed130: :: REWRITE3:79
theorem ThRed140: :: REWRITE3:80
:: deftheorem DefTran defines ==>* REWRITE3:def 6 :
theorem ThTran5: :: 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 ThTran10: :: REWRITE3:82
theorem ThTran20: :: 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 ThTran21: :: REWRITE3:84
theorem :: REWRITE3:85
theorem ThTran30: :: REWRITE3:86
theorem ThTran40: :: REWRITE3:87
theorem ThTran50: :: REWRITE3:88
theorem ThTran60: :: REWRITE3:89
theorem :: REWRITE3:90
theorem ThTran70: :: REWRITE3:91
theorem ThTran80: :: REWRITE3:92
theorem ThTran90: :: 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 DefAcc defines ==>* REWRITE3:def 7 :
theorem ThAcc5: :: REWRITE3:94
theorem ThAcc10: :: REWRITE3:95
theorem ThAcc20: :: REWRITE3:96
theorem :: REWRITE3:97
theorem :: REWRITE3:98
theorem :: REWRITE3:99
theorem ThAcc50: :: REWRITE3:100
theorem :: REWRITE3:101
theorem :: REWRITE3:102
:: deftheorem defines -succ_of REWRITE3:def 8 :
theorem ThSucc10: :: REWRITE3:103
theorem :: REWRITE3:104
theorem :: REWRITE3:105