-
Notifications
You must be signed in to change notification settings - Fork 0
/
m1_programmes.bpo
356 lines (356 loc) · 65.5 KB
/
m1_programmes.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
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
<?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="USER" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.poIdentifier name="PROGRAMME" org.eventb.core.type="ℙ(PROGRAMME)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="administrators" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="logged_in" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.poIdentifier name="programme_leader" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="programmes" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="published" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="registered" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.poPredicate name="programme_leades" org.eventb.core.predicate="registered⊆USER" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.invariant#_QUDCYEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="programme_leadet" org.eventb.core.predicate="logged_in⊆registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.invariant#_QUDpcEHEEeqKzaOTi1o2gg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="INITIALISATION/inv12/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leades"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(PROGRAMME×USER))∈(∅ ⦂ ℙ(PROGRAMME)) → (∅ ⦂ ℙ(USER))" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#INITIALISATION\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv13/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leades"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(PROGRAMME×USER))∈(∅ ⦂ ℙ(PROGRAMME)) ↔ (∅ ⦂ ℙ(USER))" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#INITIALISATION\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv14/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leades"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(PROGRAMME))⊆(∅ ⦂ ℙ(PROGRAMME))" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#INITIALISATION\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leades" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="programmes'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="published'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.poIdentifier name="programme_leader'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="administrators'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="logged_in'" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leades" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leades" org.eventb.core.poStamp="0"/>
<org.eventb.core.poSequent name="publish_programme/grd3/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadet("/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="p∈dom(programme_leader)∧programme_leader∈PROGRAMME ⇸ USER" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzokHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzokHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadet("/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="publish_programme/inv14/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="published∪{p}⊆programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#publish_programme\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leadet" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="published'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_leadet(" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leadet" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzoEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzoUHHEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leadet" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadet(" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="u=programme_leader(p)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzokHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_sioQokHHEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="unpublish_programme/grd3/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadeu("/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="p∈dom(programme_leader)∧programme_leader∈PROGRAMME ⇸ USER" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_mSUUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_mSUUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadeu("/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="unpublish_programme/inv14/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadeu"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="published ∖ {p}⊆programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#unpublish_programme\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leadeu" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="published'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_leadeu(" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leadeu" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_lrQEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_mSUEHHEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leadeu" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadeu(" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="u=programme_leader(p)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_mSUUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="p∈published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_3BElcEHHEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="create_programme/inv12/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="programme_leader{p ↦ u}∈programmes∪{p} → registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#create_programme\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="create_programme/inv13/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="administrators∪{p ↦ u}∈programmes∪{p} ↔ registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#create_programme\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="create_programme/inv14/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="published⊆programmes∪{p}" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#create_programme\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leadev" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="programmes'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="programme_leader'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="administrators'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leadev" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leadev" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sinpkUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="p∈PROGRAMME" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sioQoEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="p∉programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sioQoUHHEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="delete_programme/grd3/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadew("/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="p∈dom(programme_leader)∧programme_leader∈PROGRAMME ⇸ USER" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YkHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YkHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadew("/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_programme/inv12/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadew"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{p} ⩤ programme_leader∈programmes ∖ {p} → registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#delete_programme\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_programme/inv13/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadew"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{p} ⩤ administrators∈programmes ∖ {p} ↔ registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#delete_programme\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_programme/inv14/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadew"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="published⊆programmes ∖ {p}" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#delete_programme\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leadew" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="programmes'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="programme_leader'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="administrators'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_leadew(" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leadew" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YUHHEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leadew" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadew(" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="programme_leader(p)=u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YkHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nL08UHHEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="add_administrator/grd4/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadex)"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="p∈dom(programme_leader)∧programme_leader∈PROGRAMME ⇸ USER" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gpmIoEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gpmIoEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadex)"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="add_administrator/inv13/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadex"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="administrators∪{p ↦ u2}∈programmes ↔ registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#add_administrator\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leadex" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u1" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="administrators'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="u2" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_leadex)" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leadex" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nLN4UHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nLN4kHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nL08EHHEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leadex" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadex)" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gpmIoEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="u2∉administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sio3sEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_cDwN8EHIEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="remove_administrator/grd4/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadey)"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="p∈dom(programme_leader)∧programme_leader∈PROGRAMME ⇸ USER" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIkgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIkgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadey)"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="remove_administrator/inv13/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadey"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="administrators ∖ {p ↦ u2}∈programmes ↔ registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#remove_administrator\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leadey" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u1" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="administrators'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="u2" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_leadey)" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leadey" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gpk6gEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gplhkEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gplhkUgTEeqeqbGZOOBkaQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leadey" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadey)" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIkgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="u2∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BElcUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_eZxgUEc9EeqCJoBEKqsuQA"/>
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_WXhJ8EgVEeqeqbGZOOBkaQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="transfer_ownership/grd4/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadez)"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="p∈dom(programme_leader)∧programme_leader∈PROGRAMME ⇸ USER" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_aUM3YEgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_aUM3YEgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadez)"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="transfer_ownership/inv12/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leadez"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="programme_leader{p ↦ u2}∈programmes → registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#transfer_ownership\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leadez" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u1" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="programme_leader'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="u2" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_leadez)" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leadez" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW06EEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIUgTEeqeqbGZOOBkaQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leadez" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTHYPprogramme_leadez)" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_aUM3YEgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="u2∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nMcAEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_bx1dkEgVEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_bx1dkUgVEeqeqbGZOOBkaQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="register/inv12/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leade{"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="programme_leader∈programmes → registered∪{u}" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gi"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#register\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="register/inv13/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leade{"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="administrators∈programmes ↔ registered∪{u}" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gi"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#register\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leade{" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leade{" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leade{" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈USER" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQiLYUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u∉registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQiycEHEEeqKzaOTi1o2gg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="unregister/inv12/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leade\|"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="programme_leader∈programmes → registered ∖ {u}" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#unregister\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="unregister/inv13/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="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_leade\|"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="administrators∈programmes ↔ registered ∖ {u}" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poSequent#unregister\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leade|" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leade|" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leade\|" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQjZgUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u∉logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQkAkEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="u∉ran(programme_leader)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj|org.eventb.core.guard#_CWPG4EHIEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="u∉ran(administrators)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj|org.eventb.core.guard#_CWPG4UHIEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leade}" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="logged_in'" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leade}" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leade}" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqZHkUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u∉logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqZuoEHEEeqKzaOTi1o2gg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_leade~" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="logged_in'" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_leade~" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#EVTIDENTprogramme_leade~" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqaVsUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqaVskHEEeqKzaOTi1o2gg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/progmanmodel/m1_programmes.bpo|org.eventb.core.poFile#m1_programmes|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="programmes⊆PROGRAMME" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_liiugEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="programme_leader∈programmes → registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="administrators∈programmes ↔ registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="published⊆programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>