-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathm1_shafts.bpo
173 lines (173 loc) · 31.7 KB
/
m1_shafts.bpo
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="CABINS" org.eventb.core.type="ℙ(CABINS)"/>
<org.eventb.core.poIdentifier name="CABIN_FLOOR" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.poIdentifier name="FLOORS" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.poIdentifier name="TOP_FLOOR" org.eventb.core.type="ℤ"/>
<org.eventb.core.poPredicate name="CABIN_FLOOS" org.eventb.core.predicate="TOP_FLOOR∈ℕ1" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MsxEwJ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="CABIN_FLOOT" org.eventb.core.predicate="TOP_FLOOR=7" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Msxr0J6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="CABIN_FLOOU" org.eventb.core.predicate="FLOORS=0 ‥ TOP_FLOOR" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MsyS4J6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="CABIN_FLOOV" org.eventb.core.predicate="finite(CABINS)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_M9xTMJ7DEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="CABIN_FLOOW" org.eventb.core.predicate="card(FLOORS)=TOP_FLOOR+1" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MszhAJ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="CABIN_FLOOX" org.eventb.core.predicate="finite(FLOORS)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MszhAZ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="CABIN_FLOOY" org.eventb.core.predicate="card(CABINS)<card(FLOORS)∗2" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Rn7VMJ7DEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="CABIN_FLOOZ" org.eventb.core.predicate="CABIN_FLOOR∈CABINS → FLOORS" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Ms0vIJ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="CABIN_FLOO[" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(CABIN_FLOOR)⇒CABIN_FLOOR(c)∉ran({c} ⩤ CABIN_FLOOR)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Ms1WMJ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poIdentifier name="SHAFTS" org.eventb.core.type="ℙ(SHAFTS)"/>
<org.eventb.core.poIdentifier name="DOWN" org.eventb.core.type="SHAFTS"/>
<org.eventb.core.poIdentifier name="UP" org.eventb.core.type="SHAFTS"/>
<org.eventb.core.poPredicate name="CABIN_FLOO\" org.eventb.core.predicate="finite(SHAFTS)" org.eventb.core.source="/MULTI-Elevator/m1_shafts_context.buc|org.eventb.core.contextFile#m1_shafts_context|org.eventb.core.axiom#_Zy9zQKFQEeq6js3PozKjqQ"/>
<org.eventb.core.poPredicate name="CABIN_FLOO]" org.eventb.core.predicate="partition(SHAFTS,{UP},{DOWN})" org.eventb.core.source="/MULTI-Elevator/m1_shafts_context.buc|org.eventb.core.contextFile#m1_shafts_context|org.eventb.core.axiom#_Zy-aUKFQEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="floor" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.poIdentifier name="shaft" org.eventb.core.type="ℙ(CABINS×SHAFTS)"/>
<org.eventb.core.poPredicate name="shafu" org.eventb.core.predicate="floor∈CABINS → FLOORS" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.invariant#_aweL0J94Eeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="INITIALISATION/shaft_type/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTALLHYPm1_shafts_contexv"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="CABINS × {UP}∈CABINS → SHAFTS" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.invariant#_G2fpUJ97Eeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.invariant#_G2fpUJ97Eeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poSequent#INITIALISATION\/shaft_type\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm1_shafts_contexv" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="shaft'" org.eventb.core.type="ℙ(CABINS×SHAFTS)"/>
<org.eventb.core.poIdentifier name="floor'" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm1_shafts_contexv" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTIDENTm1_shafts_contexv" org.eventb.core.poStamp="0"/>
<org.eventb.core.poSequent name="CabinMovesDown/lower_floor_free/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexw'"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀c⦂CABINS·(c∈dom(floor)⇒c∈dom(shaft)∧shaft∈CABINS ⇸ SHAFTS)∧(c∈dom(floor)∧shaft(c)=DOWN⇒cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ)" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogipcJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_r7I2IJ96Eeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogipcJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_r7I2IJ96Eeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexw'"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="CabinMovesDown/shaft_down/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexwcabip"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(shaft)∧shaft∈CABINS ⇸ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogipcJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_ogj3kJ94Eeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogipcJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_ogj3kJ94Eeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexwcabip"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm1_shafts_contexw" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="floor'" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm1_shafts_contexw'" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTIDENTm1_shafts_contexw" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="0≤floor(cabin) − 1" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#_awgBAJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_awgoEZ94Eeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm1_shafts_contexwcabip" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexw'" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(floor)∧shaft(c)=DOWN⇒floor(cabin) − 1≠floor(c)" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogipcJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_r7I2IJ96Eeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm1_shafts_contexw" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexwcabip" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="shaft(cabin)=DOWN" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogipcJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_ogj3kJ94Eeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="CabinMovesUp/upper_floor_free/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexx'"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀c⦂CABINS·(c∈dom(floor)⇒c∈dom(shaft)∧shaft∈CABINS ⇸ SHAFTS)∧(c∈dom(floor)∧shaft(c)=UP⇒cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ)" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogkeoJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_r7KEQJ96Eeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogkeoJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_r7KEQJ96Eeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexx'"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="CabinMovesUp/shaft_up/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexxcabip"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(shaft)∧shaft∈CABINS ⇸ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogkeoJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_oglswZ94Eeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogkeoJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_oglswZ94Eeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexxcabip"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm1_shafts_contexx" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="floor'" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm1_shafts_contexx'" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTIDENTm1_shafts_contexx" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="TOP_FLOOR≥floor(cabin)+1" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#_aweL0Z94Eeq6js3PozKjqQ|org.eventb.core.guard#_awey4Z94Eeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm1_shafts_contexxcabip" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexx'" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(floor)∧shaft(c)=UP⇒floor(cabin)+1≠floor(c)" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogkeoJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_r7KEQJ96Eeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm1_shafts_contexx" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexxcabip" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="shaft(cabin)=UP" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogkeoJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_oglswZ94Eeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="CabinUpToDown/at_top_floor/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTIDENTm1_shafts_contexy"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DMRoJ-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DMRoJ-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTIDENTm1_shafts_contexy"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="CabinUpToDown/in_up_shaft/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexy'"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(shaft)∧shaft∈CABINS ⇸ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DM4sJ-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DM4sJ-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexy'"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="CabinUpToDown/top_right_free/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexy("/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀c⦂CABINS·(c∈dom(shaft)⇒shaft∈CABINS ⇸ SHAFTS)∧(c∈dom(shaft)∧shaft(c)=DOWN⇒c∈dom(floor)∧floor∈CABINS ⇸ ℤ)" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DNfwJ-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DNfwJ-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexy("/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="CabinUpToDown/shaft_type/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTALLHYPm1_shafts_contexy"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="shaft{cabin ↦ DOWN}∈CABINS → SHAFTS" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.invariant#_G2fpUJ97Eeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.invariant#_G2fpUJ97Eeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poSequent#CabinUpToDown\/shaft_type\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm1_shafts_contexy" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="shaft'" org.eventb.core.type="ℙ(CABINS×SHAFTS)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm1_shafts_contexy'" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTIDENTm1_shafts_contexy" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="floor(cabin)=TOP_FLOOR" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DMRoJ-WEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm1_shafts_contexy(" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexy'" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="shaft(cabin)=UP" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DM4sJ-WEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm1_shafts_contexy" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexy(" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(shaft)∧shaft(c)=DOWN⇒floor(c)≠TOP_FLOOR" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DNfwJ-WEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="CabinDownToUp/at_ground_floor/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTIDENTm1_shafts_contexz"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DOt4J-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DOt4J-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTIDENTm1_shafts_contexz"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="CabinDownToUp/in_down_shaft/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexz'"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(shaft)∧shaft∈CABINS ⇸ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DPU8J-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DPU8J-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexz'"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="CabinDownToUp/ground_left_free/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexz("/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀c⦂CABINS·(c∈dom(shaft)⇒shaft∈CABINS ⇸ SHAFTS)∧(c∈dom(shaft)∧shaft(c)=UP⇒c∈dom(floor)∧floor∈CABINS ⇸ ℤ)" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DP8AJ-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DP8AJ-WEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexz("/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="CabinDownToUp/shaft_type/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTALLHYPm1_shafts_contexz"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="shaft{cabin ↦ UP}∈CABINS → SHAFTS" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.invariant#_G2fpUJ97Eeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.invariant#_G2fpUJ97Eeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poSequent#CabinDownToUp\/shaft_type\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm1_shafts_contexz" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="shaft'" org.eventb.core.type="ℙ(CABINS×SHAFTS)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm1_shafts_contexz'" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTIDENTm1_shafts_contexz" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="floor(cabin)=0" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DOt4J-WEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm1_shafts_contexz(" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexz'" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="shaft(cabin)=DOWN" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DPU8J-WEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm1_shafts_contexz" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#EVTHYPm1_shafts_contexz(" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(shaft)∧shaft(c)=UP⇒floor(c)≠0" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DP8AJ-WEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/MULTI-Elevator/m1_shafts.bpo|org.eventb.core.poFile#m1_shafts|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="shaft∈CABINS → SHAFTS" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.invariant#_G2fpUJ97Eeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>