-
Notifications
You must be signed in to change notification settings - Fork 0
/
m5_semesters.bcm
475 lines (475 loc) · 137 KB
/
m5_semesters.bcm
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
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
<org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.refinesMachine#'"/>
<org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/progmanmodel/c5_semesters.bcc" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.seesContext#_NQ8oUEanEeqCJoBEKqsuQA"/>
<org.eventb.core.scInternalContext name="c0_users">
<org.eventb.core.scCarrierSet name="USER" org.eventb.core.source="/progmanmodel/c0_users.buc|org.eventb.core.contextFile#c0_users|org.eventb.core.carrierSet#_swFc0EHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="c1_programmes">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/progmanmodel/c0_users.bcc|org.eventb.core.scContextFile#c0_users" org.eventb.core.source="/progmanmodel/c1_programmes.buc|org.eventb.core.contextFile#c1_programmes|org.eventb.core.extendsContext#_qcMHkEHSEeqHCPZ-G665YQ"/>
<org.eventb.core.scCarrierSet name="PROGRAMME" org.eventb.core.source="/progmanmodel/c1_programmes.buc|org.eventb.core.contextFile#c1_programmes|org.eventb.core.carrierSet#_qcMuoEHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(PROGRAMME)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="c2_modules">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/progmanmodel/c1_programmes.bcc|org.eventb.core.scContextFile#c1_programmes" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.extendsContext#_fuhrAEHSEeqHCPZ-G665YQ"/>
<org.eventb.core.scAxiom name="c1_programmet" org.eventb.core.label="axm21" org.eventb.core.predicate="credits={15,30,45,60}" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_rGOvUUgCEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="c1_programmeu" org.eventb.core.label="axm22" org.eventb.core.predicate="sum∈(MODULE ↔ credits) → ℕ" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_Ut5fQE5AEeqUxct8tLY9IA" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="c1_programmev" org.eventb.core.label="axm23" org.eventb.core.predicate="sum(∅ ⦂ ℙ(MODULE×ℤ))=0" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_Ut5fQU5AEeqUxct8tLY9IA" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="c1_programmew" org.eventb.core.label="sum24" org.eventb.core.predicate="∀f⦂ℙ(MODULE×ℤ),m⦂MODULE·f∈MODULE ⇸ credits∧m∈dom(f)⇒sum(f)=sum({m} ⩤ f)+f(m)" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_duc5wE5AEeqUxct8tLY9IA" org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="MODULE" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.carrierSet#_fuiSEEHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(MODULE)"/>
<org.eventb.core.scConstant name="credits" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.constant#_rGOvUEgCEeqeqbGZOOBkaQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scConstant name="sum" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.constant#_Ut44ME5AEeqUxct8tLY9IA" org.eventb.core.type="ℙ(ℙ(MODULE×ℤ)×ℤ)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="c3_outcomes">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/progmanmodel/c2_modules.bcc|org.eventb.core.scContextFile#c2_modules" org.eventb.core.source="/progmanmodel/c3_outcomes.buc|org.eventb.core.contextFile#c3_outcomes|org.eventb.core.extendsContext#'"/>
<org.eventb.core.scCarrierSet name="M_OUTCOME" org.eventb.core.source="/progmanmodel/c3_outcomes.buc|org.eventb.core.contextFile#c3_outcomes|org.eventb.core.carrierSet#_HOa80EHTEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(M_OUTCOME)"/>
<org.eventb.core.scCarrierSet name="P_OUTCOME" org.eventb.core.source="/progmanmodel/c3_outcomes.buc|org.eventb.core.contextFile#c3_outcomes|org.eventb.core.carrierSet#_HObj4EHTEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(P_OUTCOME)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="c4_prerequisites">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/progmanmodel/c3_outcomes.bcc|org.eventb.core.scContextFile#c3_outcomes" org.eventb.core.source="/progmanmodel/c4_prerequisites.buc|org.eventb.core.contextFile#c4_prerequisites|org.eventb.core.extendsContext#'"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="c5_semesters">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/progmanmodel/c4_prerequisites.bcc|org.eventb.core.scContextFile#c4_prerequisites" org.eventb.core.source="/progmanmodel/c5_semesters.buc|org.eventb.core.contextFile#c5_semesters|org.eventb.core.extendsContext#'"/>
<org.eventb.core.scAxiom name="c4_prerequisitet" org.eventb.core.label="axm51" org.eventb.core.predicate="semester={1,2}" org.eventb.core.source="/progmanmodel/c5_semesters.buc|org.eventb.core.contextFile#c5_semesters|org.eventb.core.axiom#_aP8HoEgCEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="c4_prerequisiteu" org.eventb.core.label="axm52" org.eventb.core.predicate="year={1,2,3,4}" org.eventb.core.source="/progmanmodel/c5_semesters.buc|org.eventb.core.contextFile#c5_semesters|org.eventb.core.axiom#_aP8HoUgCEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="SEMESTER" org.eventb.core.source="/progmanmodel/c5_semesters.buc|org.eventb.core.contextFile#c5_semesters|org.eventb.core.carrierSet#_sTDq8EamEeqCJoBEKqsuQA" org.eventb.core.type="ℙ(SEMESTER)"/>
<org.eventb.core.scCarrierSet name="YEAR" org.eventb.core.source="/progmanmodel/c5_semesters.buc|org.eventb.core.contextFile#c5_semesters|org.eventb.core.carrierSet#_efDTEEanEeqCJoBEKqsuQA" org.eventb.core.type="ℙ(YEAR)"/>
<org.eventb.core.scConstant name="semester" org.eventb.core.source="/progmanmodel/c5_semesters.buc|org.eventb.core.contextFile#c5_semesters|org.eventb.core.constant#_dvYQAEavEeqCJoBEKqsuQA" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scConstant name="year" org.eventb.core.source="/progmanmodel/c5_semesters.buc|org.eventb.core.contextFile#c5_semesters|org.eventb.core.constant#_dvY3EEavEeqCJoBEKqsuQA" org.eventb.core.type="ℙ(ℤ)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="c0_usert" org.eventb.core.label="inv1" 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.theorem="false"/>
<org.eventb.core.scInvariant name="c0_useru" org.eventb.core.label="inv2" 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.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmet" org.eventb.core.label="inv11" 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.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmeu" org.eventb.core.label="inv12" 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.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmev" org.eventb.core.label="inv13" 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.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmew" org.eventb.core.label="inv14" 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.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmex" org.eventb.core.label="inv21" org.eventb.core.predicate="modules⊆MODULE" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.invariant#_AGHo8UHJEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmey" org.eventb.core.label="inv22" org.eventb.core.predicate="contains_module∈programmes ↔ modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.invariant#_FmSs8EHJEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmez" org.eventb.core.label="inv23" org.eventb.core.predicate="module_leader∈modules → registered" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.invariant#_FmSs8UHJEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programme{" org.eventb.core.label="inv24" org.eventb.core.predicate="credits_awarded∈modules → credits" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.invariant#_2Be78EgCEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programme|" org.eventb.core.label="inv25" org.eventb.core.predicate="credits_awarded∈MODULE ⇸ credits" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.invariant#_dxz9oFGfEeq01sNmetMbsA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programme}" org.eventb.core.label="inv31" org.eventb.core.predicate="programme_outcomes∈programmes ↔ P_OUTCOME" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.invariant#_ksiyQEHUEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programme~" org.eventb.core.label="inv32" org.eventb.core.predicate="module_outcomes∈modules ↔ M_OUTCOME" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.invariant#_Jmq7sEHVEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmf'" org.eventb.core.label="inv33" org.eventb.core.predicate="outcome_mapping∈module_outcomes ↔ programme_outcomes" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.invariant#_Jmq7sUHVEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmf(" org.eventb.core.label="inv34" org.eventb.core.predicate="∀m⦂MODULE·m∈dom(dom(outcome_mapping))⇒dom(ran(({m} ◁ dom(outcome_mapping)) ◁ outcome_mapping))⊆contains_module∼[{m}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.invariant#_OHoTEEmkEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmf)" org.eventb.core.label="inv41" org.eventb.core.predicate="prerequisites∈modules ↔ modules" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.invariant#_80wkoUJyEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmf*" org.eventb.core.label="inv42" org.eventb.core.predicate="∀p⦂PROGRAMME,m⦂MODULE·p∈published∧m∈contains_module[{p}]⇒prerequisites[{m}]⊆contains_module[{p}]" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.invariant#_lUfGUEJ0EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c4_prerequisitet" org.eventb.core.label="inv51" org.eventb.core.predicate="programme_duration∈programmes → year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxkkJ6EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c4_prerequisiteu" org.eventb.core.label="inv52" org.eventb.core.predicate="module_semester∈modules → semester" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxk0J6EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c4_prerequisitev" org.eventb.core.label="inv53" org.eventb.core.predicate="module_year∈modules → year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_Zoo9wEanEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c4_prerequisitew" org.eventb.core.label="inv54" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆modules∧m2∈prerequisites[{m1}]⇒module_year(m1)≥module_year(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c4_prerequisitex" org.eventb.core.label="inv55" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆modules∧m2∈prerequisites[{m1}]∧module_year(m1)=module_year(m2)⇒module_semester(m1)>module_semester(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c4_prerequisitey" org.eventb.core.label="inv56" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈published∧s∈semester∧y∈year⇒sum((contains_module[{p}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≥30" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="administrators" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_vN_gIUHGEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.scVariable name="contains_module" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_AGHB4UHJEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.scVariable name="credits_awarded" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_I--HYEgIEeqeqbGZOOBkaQ" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.scVariable name="logged_in" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_MTJYwEHEEeqKzaOTi1o2gg" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.scVariable name="module_leader" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_AGHo8EHJEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(MODULE×USER)"/>
<org.eventb.core.scVariable name="module_outcomes" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_ksiLMEHUEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(MODULE×M_OUTCOME)"/>
<org.eventb.core.scVariable name="module_semester" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_NRL44EanEeqCJoBEKqsuQA" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.scVariable name="module_year" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_ZooWsEanEeqCJoBEKqsuQA" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.scVariable name="modules" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_AGHB4EHJEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(MODULE)"/>
<org.eventb.core.scVariable name="outcome_mapping" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_ksiLMkHUEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
<org.eventb.core.scVariable name="prerequisites" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_80wkoEJyEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(MODULE×MODULE)"/>
<org.eventb.core.scVariable name="programme_duration" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_cOgxkEJ6EeqHCPZ-G665YQ" org.eventb.core.type="ℙ(PROGRAMME×ℤ)"/>
<org.eventb.core.scVariable name="programme_leader" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_vN_gIEHGEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.scVariable name="programme_outcomes" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_ksiLMUHUEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(PROGRAMME×P_OUTCOME)"/>
<org.eventb.core.scVariable name="programmes" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_iY418EHGEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.scVariable name="published" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_Jd3MYEgUEeqeqbGZOOBkaQ" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.scVariable name="registered" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.variable#_MTIxsEHEEeqKzaOTi1o2gg" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.scEvent name="programme_outcomet" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomet" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.scAction name="'" org.eventb.core.assignment="registered ≔ ∅ ⦂ ℙ(USER)" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#'|org.eventb.core.action#_TSDroEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="logged_in ≔ ∅ ⦂ ℙ(USER)" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#'|org.eventb.core.action#_TSESsEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="programmes ≔ ∅ ⦂ ℙ(PROGRAMME)" org.eventb.core.label="act11" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_0s5_4EHGEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="programme_leader ≔ ∅ ⦂ ℙ(PROGRAMME×USER)" org.eventb.core.label="act12" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_0s5_4UHGEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="administrators ≔ ∅ ⦂ ℙ(PROGRAMME×USER)" org.eventb.core.label="act13" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_0s5_4kHGEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="," org.eventb.core.assignment="published ≔ ∅ ⦂ ℙ(PROGRAMME)" org.eventb.core.label="act14" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_3ZnrMEgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.scAction name="-" org.eventb.core.assignment="modules ≔ ∅ ⦂ ℙ(MODULE)" org.eventb.core.label="act21" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_LP_gYEHJEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="." org.eventb.core.assignment="contains_module ≔ ∅ ⦂ ℙ(PROGRAMME×MODULE)" org.eventb.core.label="act22" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_LP_gYUHJEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="/" org.eventb.core.assignment="module_leader ≔ ∅ ⦂ ℙ(MODULE×USER)" org.eventb.core.label="act23" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_LQAHcEHJEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="0" org.eventb.core.assignment="credits_awarded ≔ ∅ ⦂ ℙ(MODULE×ℤ)" org.eventb.core.label="act24" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_5qwvwEgCEeqeqbGZOOBkaQ"/>
<org.eventb.core.scAction name="1" org.eventb.core.assignment="programme_outcomes ≔ ∅ ⦂ ℙ(PROGRAMME×P_OUTCOME)" org.eventb.core.label="act31" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_StTwEEHVEeqHCPZ-G665YQ"/>
<org.eventb.core.scAction name="2" org.eventb.core.assignment="module_outcomes ≔ ∅ ⦂ ℙ(MODULE×M_OUTCOME)" org.eventb.core.label="act32" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_StTwEUHVEeqHCPZ-G665YQ"/>
<org.eventb.core.scAction name="3" org.eventb.core.assignment="outcome_mapping ≔ ∅ ⦂ ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))" org.eventb.core.label="act33" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_StTwEkHVEeqHCPZ-G665YQ"/>
<org.eventb.core.scAction name="4" org.eventb.core.assignment="prerequisites ≔ ∅ ⦂ ℙ(MODULE×MODULE)" org.eventb.core.label="act41" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#__qLSkEJyEeqHCPZ-G665YQ"/>
<org.eventb.core.scAction name="5" org.eventb.core.assignment="programme_duration ≔ ∅ ⦂ ℙ(PROGRAMME×ℤ)" org.eventb.core.label="act51" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_hDIXIEJ6EeqHCPZ-G665YQ"/>
<org.eventb.core.scAction name="6" org.eventb.core.assignment="module_semester ≔ ∅ ⦂ ℙ(MODULE×ℤ)" org.eventb.core.label="act52" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_hDI-MEJ6EeqHCPZ-G665YQ"/>
<org.eventb.core.scAction name="7" org.eventb.core.assignment="module_year ≔ ∅ ⦂ ℙ(MODULE×ℤ)" org.eventb.core.label="act53" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_p8vPoEatEeqCJoBEKqsuQA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomeu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="change_semester" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.guard#_tmrS4Ec-EeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.guard#_tmrS4Uc-EeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="s∈semester" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.guard#_tmr58Ec-EeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u=module_leader(m)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.guard#_tmr58Uc-EeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="module_semester(m)≠s" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.guard#_AKSYAEc_EeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="∀m2⦂MODULE·m2∈modules∧m2∈prerequisites[{m}]∧module_year(m)=module_year(m2)⇒s>module_semester(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.guard#_Uj4VEEdEEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="∀m2⦂MODULE·m2∈modules∧m∈prerequisites[{m2}]∧module_year(m)=module_year(m2)⇒s<module_semester(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.guard#_Uj4VEUdEEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="grd8" org.eventb.core.predicate="m∉contains_module[published]" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.guard#_30zs8EjBEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="/" org.eventb.core.label="grd9" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s1⦂ℤ·p∈published∧s1∈semester∧y∈year⇒sum((contains_module[{p}]∩module_year∼[{y}]∩(module_semester{m ↦ s})∼[{s1}]) ◁ credits_awarded)≥30" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.guard#_iewJYGkCEeqIPJEEodEg6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.parameter#_tmqr0Uc-EeqCJoBEKqsuQA" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="s" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.parameter#_l1XVIEauEeqCJoBEKqsuQA" org.eventb.core.type="ℤ"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.parameter#_ienmgGkCEeqIPJEEodEg6Q" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="module_semester ≔ module_semester{m ↦ s}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA|org.eventb.core.action#_DwGBEEc_EeqCJoBEKqsuQA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomev" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="change_year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_x1hKgEdBEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_x1hKgUdBEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="y∈year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_x1hxkEdBEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u=module_leader(m)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_x1hxkUdBEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="module_year(m)≠y" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_zT5tkEjBEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="∀m2⦂MODULE·m2∈modules∧m2∈prerequisites[{m}]⇒module_year(m2)≤y" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_8Gra8Eg2EeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="∀m2⦂MODULE·m2∈modules∧m∈prerequisites[{m2}]⇒module_year(m2)≥y" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_8Gra8Ug2EeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="grd8" org.eventb.core.predicate="∀m2⦂MODULE·m2∈modules∧m2∈prerequisites[{m}]∧y=module_year(m2)⇒module_semester(m)>module_semester(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_5H-LsEjGEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="/" org.eventb.core.label="grd9" org.eventb.core.predicate="∀m2⦂MODULE·m2∈modules∧m∈prerequisites[{m2}]∧y=module_year(m2)⇒module_semester(m)<module_semester(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_ooGKEI79Eeq1J8HIGUp2sw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="0" org.eventb.core.label="grd10" org.eventb.core.predicate="∀d⦂ℤ·d∈programme_duration[contains_module∼[{m}]]⇒d≥y" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_iewwcGkCEeqIPJEEodEg6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="1" org.eventb.core.label="grd11" org.eventb.core.predicate="m∉contains_module[published]" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_iexXgGkCEeqIPJEEodEg6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="2" org.eventb.core.label="grd12" org.eventb.core.predicate="∀p⦂PROGRAMME,y1⦂ℤ,s⦂ℤ·p∈published∧s∈semester∧y1∈year⇒sum((contains_module[{p}]∩(module_year{m ↦ y})∼[{y1}]∩module_semester∼[{s}]) ◁ credits_awarded)≥30" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_vW8AoI79Eeq1J8HIGUp2sw" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.parameter#_x1gjcUdBEeqCJoBEKqsuQA" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.parameter#_iesfAGkCEeqIPJEEodEg6Q" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="y" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.parameter#_l1X8MEauEeqCJoBEKqsuQA" org.eventb.core.type="ℤ"/>
<org.eventb.core.scAction name="z" org.eventb.core.assignment="module_year ≔ module_year{m ↦ y}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA|org.eventb.core.action#_ZuqX4EdEEeqCJoBEKqsuQA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomew" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="change_duration" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_Tr_Y4UdGEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_Tr__8EdGEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="d∈year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_Tr__8UdGEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_iezzwGkCEeqIPJEEodEg6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="d≠programme_duration(p)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_ie0a0GkCEeqIPJEEodEg6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="contains_module[{p}]⊆module_year∼[{x⦂ℤ·x∈year∧x≤d ∣ x}]" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_45i7cGkCEeqIPJEEodEg6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.guard#_45jigGkCEeqIPJEEodEg6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="d" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.parameter#_uRmuIEJ7EeqHCPZ-G665YQ" org.eventb.core.type="ℤ"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.parameter#_Tr_Y4EdGEeqCJoBEKqsuQA" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.parameter#_iex-kGkCEeqIPJEEodEg6Q" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="programme_duration ≔ programme_duration{p ↦ d}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA|org.eventb.core.action#_X8HKQEdGEeqCJoBEKqsuQA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomex" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="publish_programme" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk33wEgUEeqeqbGZOOBkaQ">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomew" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk33wEgUEeqeqbGZOOBkaQ|org.eventb.core.refinesEvent#_Kk4e0EgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" 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.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" 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.theorem="false"/>
<org.eventb.core.scGuard name="w" org.eventb.core.label="grd31" org.eventb.core.predicate="∀po⦂P_OUTCOME·po∈programme_outcomes[{p}]⇒outcome_mapping ▷ {p ↦ po}≠(∅ ⦂ ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME)))" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_7Y1LYEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_biA3wEmoEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="x" org.eventb.core.label="grd41" org.eventb.core.predicate="∀m⦂MODULE·m∈contains_module[{p}]⇒prerequisites[{m}]⊆contains_module[{p}]" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_EVzGYEgUEeqeqbGZOOBkaQ|org.eventb.core.guard#_IanikEJ1EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="published ≔ published∪{p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.action#_JVrasEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_JVqMkkHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_JVqMkUHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scGuard name="y" org.eventb.core.label="grd51" org.eventb.core.predicate="∀y⦂ℤ,s⦂ℤ·s∈semester∧y∈year⇒sum((contains_module[{p}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≥30" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk33wEgUEeqeqbGZOOBkaQ|org.eventb.core.guard#_uRmuIUJ7EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomey" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unpublish_programme" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk4e0UgUEeqeqbGZOOBkaQ">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomex" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk4e0UgUEeqeqbGZOOBkaQ|org.eventb.core.refinesEvent#_Kk4e0kgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" 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.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" 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.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="published ≔ published ∖ {p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.action#_g_m5YEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_ROOEQEHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_RONdMEHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomez" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="assign_prerequisite" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomeu" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd41" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_4vYOMEJzEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd42" org.eventb.core.predicate="m1∈modules" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_4vYOMUJzEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd43" org.eventb.core.predicate="m2∈modules" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_4vY1QEJzEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd44" org.eventb.core.predicate="u=module_leader(m1)" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_4vY1QUJzEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd47" org.eventb.core.predicate="m2∉prerequisites[{m1}]" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_MckKgEJ0EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd48" org.eventb.core.predicate="m1≠m2" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_Tmo70EKFEeqP-97FScFUgw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd49" org.eventb.core.predicate="m1∉contains_module[published]" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_S7ILgEgpEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="grd50" org.eventb.core.predicate="m1∉prerequisites[{m2}]" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_LqBnUI70Eeq1J8HIGUp2sw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="m3" org.eventb.core.assignment="prerequisites ≔ prerequisites∪{m1 ↦ m2}" org.eventb.core.label="act41" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.action#_MckKgUJ0EeqHCPZ-G665YQ"/>
<org.eventb.core.scParameter name="m1" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.parameter#_4vXnIUJzEeqHCPZ-G665YQ" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="m2" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.parameter#_4vXnIkJzEeqHCPZ-G665YQ" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ|org.eventb.core.parameter#_4vXnIEJzEeqHCPZ-G665YQ" org.eventb.core.type="USER"/>
<org.eventb.core.scGuard name="m4" org.eventb.core.label="grd51" org.eventb.core.predicate="module_year(m2)≤module_year(m1)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi|org.eventb.core.guard#_0CJegEJ9EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="m5" org.eventb.core.label="grd52" org.eventb.core.predicate="module_year(m2)=module_year(m1)⇒module_semester(m2)<module_semester(m1)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi|org.eventb.core.guard#_l1YjQEauEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcome{" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unassign_prerequisite" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomev" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd41" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_70RGEEJ0EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd42" org.eventb.core.predicate="m1∈modules" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_70RGEUJ0EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd43" org.eventb.core.predicate="m2∈modules" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_70RGEkJ0EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd44" org.eventb.core.predicate="u=module_leader(m1)" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_70RtIEJ0EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd47" org.eventb.core.predicate="m2∈prerequisites[{m1}]" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_70RtIUJ0EeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd48" org.eventb.core.predicate="m1∉contains_module[published]" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ|org.eventb.core.guard#_UiGJUEgpEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="m3" org.eventb.core.assignment="prerequisites ≔ prerequisites ∖ {m1 ↦ m2}" org.eventb.core.label="act41" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ|org.eventb.core.action#_70RtIkJ0EeqHCPZ-G665YQ"/>
<org.eventb.core.scParameter name="m1" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ|org.eventb.core.parameter#_70QfAUJ0EeqHCPZ-G665YQ" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="m2" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ|org.eventb.core.parameter#_70QfAkJ0EeqHCPZ-G665YQ" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ|org.eventb.core.parameter#_70QfAEJ0EeqHCPZ-G665YQ" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcome|" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="assign_programme_outcome" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHk">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomey" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHk|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOilsEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOjMw0HWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOilsEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOka4EHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="o∈P_OUTCOME" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOilsEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOka4UHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOilsEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOlB8EHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="o∉programme_outcomes[{p}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOilsEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOlB8UHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOilsEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_q4AGQEgnEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="programme_outcomes ≔ programme_outcomes∪{p ↦ o}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOilsEHWEeqHCPZ-G665YQ|org.eventb.core.action#_WOlB8kHWEeqHCPZ-G665YQ"/>
<org.eventb.core.scParameter name="o" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOilsEHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_WOjMwkHWEeqHCPZ-G665YQ" org.eventb.core.type="P_OUTCOME"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOilsEHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_WOjMwUHWEeqHCPZ-G665YQ" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOilsEHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_WOjMwEHWEeqHCPZ-G665YQ" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcome}" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unassign_programme_outcome" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHl">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomez" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHl|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOmQEUHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOmQEkHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="o∈P_OUTCOME" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOm3IEHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOm3IUHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="o∈programme_outcomes[{p}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOm3IkHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.guard#_tHsQ8EgnEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="programme_outcomes ≔ programme_outcomes ∖ {p ↦ o}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.action#_WOneMEHWEeqHCPZ-G665YQ"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="outcome_mapping ≔ outcome_mapping ⩥ (ran(outcome_mapping) ▷ {o})" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.action#_Mf95EEmhEeqDwOH5c8gGmw"/>
<org.eventb.core.scParameter name="o" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.parameter#_WOmQEEHWEeqHCPZ-G665YQ" org.eventb.core.type="P_OUTCOME"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.parameter#_WOlpAUHWEeqHCPZ-G665YQ" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOlB80HWEeqHCPZ-G665YQ|org.eventb.core.parameter#_WOlpAEHWEeqHCPZ-G665YQ" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcome~" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="assign_module_outcome" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHm">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcome{" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHm|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOneMUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOosUkHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOneMUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOpTYEHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="o∈M_OUTCOME" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOneMUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOpTYUHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u=module_leader(m)" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOneMUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOpTYkHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="o∉module_outcomes[{m}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOneMUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOpTY0HWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="m∉contains_module[published]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOneMUHWEeqHCPZ-G665YQ|org.eventb.core.guard#__Ke6AEjBEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="module_outcomes ≔ module_outcomes∪{m ↦ o}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOneMUHWEeqHCPZ-G665YQ|org.eventb.core.action#_WOpTZEHWEeqHCPZ-G665YQ"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOneMUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_gsP6sEHWEeqHCPZ-G665YQ" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="o" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOneMUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_WOosUUHWEeqHCPZ-G665YQ" org.eventb.core.type="M_OUTCOME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOneMUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_WOneMkHWEeqHCPZ-G665YQ" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf'" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unassign_module_outcome" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHn">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcome\|" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHn|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOp6c0HWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOqhgEHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="o∈M_OUTCOME" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOqhgUHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u=module_leader(m)" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOrIkEHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="o∈module_outcomes[{m}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_WOrIkUHWEeqHCPZ-G665YQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="m∉contains_module[published]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.guard#__KgvMEjBEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="module_outcomes ≔ module_outcomes ∖ {m ↦ o}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.action#_WOrIkkHWEeqHCPZ-G665YQ"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="outcome_mapping ≔ (dom(outcome_mapping) ▷ {o}) ⩤ outcome_mapping" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.action#_qP2pYEmhEeqDwOH5c8gGmw"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_gsSW8EHWEeqHCPZ-G665YQ" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="o" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_WOp6ckHWEeqHCPZ-G665YQ" org.eventb.core.type="M_OUTCOME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOpTZUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_WOp6cEHWEeqHCPZ-G665YQ" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf(" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="map_outcome" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcome}" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_t9rBQEgoEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_t9roUEgoEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="po∈P_OUTCOME" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_t9roUUgoEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_t9roUkgoEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="mo∈M_OUTCOME" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_t9sPYEgoEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="m∈contains_module[{p}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_KEDFsEmgEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_KEDFsUmgEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="grd8" org.eventb.core.predicate="po∈programme_outcomes[{p}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_KEDFskmgEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="/" org.eventb.core.label="grd9" org.eventb.core.predicate="mo∈module_outcomes[{m}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_k8uYUEmgEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="0" org.eventb.core.label="grd10" org.eventb.core.predicate="m ↦ mo ↦ (p ↦ po)∉outcome_mapping" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_Wj4i4GeOEeqknqZz0CExqw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="1" org.eventb.core.label="grd11" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.guard#_hHHgsGkFEeqIPJEEodEg6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="pp" org.eventb.core.assignment="outcome_mapping ≔ outcome_mapping∪{m ↦ mo ↦ (p ↦ po)}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.action#_t9sPYUgoEeqeqbGZOOBkaQ"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_KEBQgEmgEeqDwOH5c8gGmw" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="mo" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_3uyg4EHkEeqHCPZ-G665YQ" org.eventb.core.type="M_OUTCOME"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_KEBQgUmgEeqDwOH5c8gGmw" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="po" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_3uyg4UHkEeqHCPZ-G665YQ" org.eventb.core.type="P_OUTCOME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoEHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_b8VxgEgiEeqeqbGZOOBkaQ" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf)" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unmap_outcome" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcome~" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_wKL8IEgoEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_wKL8IUgoEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="po∈P_OUTCOME" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_wKL8IkgoEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_wKMjMEgoEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="mo∈M_OUTCOME" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_aUcyEEmgEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="m∈contains_module[{p}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_aUdZIEmgEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_aUdZIUmgEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="grd8" org.eventb.core.predicate="po∈programme_outcomes[{p}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_aUdZIkmgEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="/" org.eventb.core.label="grd9" org.eventb.core.predicate="mo∈module_outcomes[{m}]" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_l__zMEmgEeqDwOH5c8gGmw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="0" org.eventb.core.label="grd10" org.eventb.core.predicate="m ↦ mo ↦ (p ↦ po)∈outcome_mapping" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_FPt28GePEeqknqZz0CExqw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="1" org.eventb.core.label="grd11" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.guard#_j08Y4GkFEeqIPJEEodEg6Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="pp" org.eventb.core.assignment="outcome_mapping ≔ outcome_mapping ∖ {m ↦ mo ↦ (p ↦ po)}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.action#_aUeAMEmgEeqDwOH5c8gGmw"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_aUbj8UmgEeqDwOH5c8gGmw" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="mo" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_69Jrk0HqEeqHCPZ-G665YQ" org.eventb.core.type="M_OUTCOME"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_aUcLAEmgEeqDwOH5c8gGmw" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="po" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_69KSoEHqEeqHCPZ-G665YQ" org.eventb.core.type="P_OUTCOME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_WOrvoUHWEeqHCPZ-G665YQ|org.eventb.core.parameter#_aUbj8EmgEeqDwOH5c8gGmw" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf*" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="create_module" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf'" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_n5An4kHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈MODULE" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_n5BO8EHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="c∈credits" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_n5BO8UHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="m∉modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qbBUUHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="modules ≔ modules∪{m}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.action#_n5B2AEHMEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="module_leader ≔ module_leader{m ↦ u}" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.action#_n5B2AUHMEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="credits_awarded ≔ credits_awarded{m ↦ c}" org.eventb.core.label="act3" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.action#_BcveUEgDEeqeqbGZOOBkaQ"/>
<org.eventb.core.scAction name="y" org.eventb.core.assignment="prerequisites ≔ {m} ⩤ prerequisites ⩥ {m}" org.eventb.core.label="act41" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo|org.eventb.core.action#_AqyJEEJ1EeqHCPZ-G665YQ"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_2BPrYEgCEeqeqbGZOOBkaQ" org.eventb.core.type="ℤ"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_n5An4UHMEeqHd7PiYTbxHg" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_n5An4EHMEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scGuard name="z" org.eventb.core.label="grd51" org.eventb.core.predicate="s∈semester" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq|org.eventb.core.guard#_l1bmkEauEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="{" org.eventb.core.label="grd52" org.eventb.core.predicate="y∈year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq|org.eventb.core.guard#_Bm-e0EdHEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="|" org.eventb.core.label="grd53" org.eventb.core.predicate="∀p⦂PROGRAMME,y1⦂ℤ,s1⦂ℤ·p∈published∧s1∈semester∧y1∈year⇒sum((contains_module[{p}]∩(module_year{m ↦ y})∼[{y1}]∩(module_semester{m ↦ s})∼[{s1}]) ◁ (credits_awarded{m ↦ c}))≥30" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq|org.eventb.core.guard#_g5yIoI7_Eeq1J8HIGUp2sw" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="s" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq|org.eventb.core.parameter#_tmu9QEc-EeqCJoBEKqsuQA" org.eventb.core.type="ℤ"/>
<org.eventb.core.scParameter name="y" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq|org.eventb.core.parameter#_x1mDAEdBEeqCJoBEKqsuQA" org.eventb.core.type="ℤ"/>
<org.eventb.core.scAction name="}" org.eventb.core.assignment="module_semester ≔ module_semester{m ↦ s}" org.eventb.core.label="act51" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq|org.eventb.core.action#_KjRpcEJ7EeqHCPZ-G665YQ"/>
<org.eventb.core.scAction name="~" org.eventb.core.assignment="module_year ≔ module_year{m ↦ y}" org.eventb.core.label="act52" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq|org.eventb.core.action#_yvIpYEJ7EeqHCPZ-G665YQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf+" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="delete_module" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHr">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf(" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHr|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_uxVxokHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_uxWYsEHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="module_leader(m)=u" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_uxWYsUHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="m∉ran(contains_module)" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMTiwUHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="{" org.eventb.core.label="grd41" org.eventb.core.predicate="m∉ran(prerequisites)" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp|org.eventb.core.guard#_zr33AI7xEeq1J8HIGUp2sw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="modules ≔ modules ∖ {m}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.action#_uxWYskHMEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="module_leader ≔ {m} ⩤ module_leader" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.action#_uxW_wEHMEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="credits_awarded ≔ {m} ⩤ credits_awarded" org.eventb.core.label="act3" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.action#_1tqOwEgHEeqeqbGZOOBkaQ"/>
<org.eventb.core.scAction name="y" org.eventb.core.assignment="outcome_mapping ≔ ({m} ◁ module_outcomes) ⩤ outcome_mapping" org.eventb.core.label="act31" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj|org.eventb.core.action#_GAwEQEHdEeqHCPZ-G665YQ"/>
<org.eventb.core.scAction name="z" org.eventb.core.assignment="module_outcomes ≔ {m} ⩤ module_outcomes" org.eventb.core.label="act32" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj|org.eventb.core.action#_C8oFIEmiEeqDwOH5c8gGmw"/>
<org.eventb.core.scAction name="|" org.eventb.core.assignment="prerequisites ≔ {m} ⩤ prerequisites" org.eventb.core.label="act41" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp|org.eventb.core.action#_eq37wEJ5EeqHCPZ-G665YQ"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_uxVxoUHMEeqHd7PiYTbxHg" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_uxVxoEHMEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scGuard name="}" org.eventb.core.label="grd51" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈published∧s∈semester∧y∈year⇒sum((contains_module[{p}]∩({m} ⩤ module_year)∼[{y}]∩({m} ⩤ module_semester)∼[{s}]) ◁ credits_awarded)≥30" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHr|org.eventb.core.guard#_5_mkYEavEeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="~" org.eventb.core.assignment="module_semester ≔ {m} ⩤ module_semester" org.eventb.core.label="act51" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHr|org.eventb.core.action#_l1ZxYEauEeqCJoBEKqsuQA"/>
<org.eventb.core.scAction name="''" org.eventb.core.assignment="module_year ≔ {m} ⩤ module_year" org.eventb.core.label="act52" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHr|org.eventb.core.action#_fFqS8EJ8EeqHCPZ-G665YQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf," org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="assign_module" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHs">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHs|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qaaQEHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qaaQUHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qbBUEHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMVX8UHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd6" org.eventb.core.predicate="m∉contains_module[{p}]" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qboYEHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd7" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_K8nhAEgiEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="contains_module ≔ contains_module∪{p ↦ m}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.action#_B5a1wEHNEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_8qZzMUHMEeqHd7PiYTbxHg" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_8qZzMkHMEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_8qZzMEHMEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scGuard name="w" org.eventb.core.label="grd51" org.eventb.core.predicate="module_year(m)≤programme_duration(p)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHs|org.eventb.core.guard#_zxg14I76Eeq1J8HIGUp2sw" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf-" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unassign_module" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf*" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMS7sEHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMS7sUHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMTiwEHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_rcwJgEHOEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="m∈contains_module[{p}]" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qbBUkHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_K8pWMEgiEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="contains_module ≔ contains_module ∖ {p ↦ m}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.action#_xMUJ0EHNEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="outcome_mapping ≔ outcome_mapping ∖ (({m} ◁ dom(outcome_mapping)) ◁ outcome_mapping ▷ ({p} ◁ ran(outcome_mapping)))" org.eventb.core.label="act31" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHl|org.eventb.core.action#_klfEkEJvEeqHCPZ-G665YQ"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMSUoUHNEeqHd7PiYTbxHg" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMSUokHNEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMSUoEHNEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scGuard name="x" org.eventb.core.label="grd51" org.eventb.core.predicate="∀p1⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p1∈published∧s∈semester∧y∈year⇒sum(((contains_module ∖ {p ↦ m})[{p1}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≥30" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt|org.eventb.core.guard#_7dt6UI7_Eeq1J8HIGUp2sw" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf." org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="transfer_module_ownership" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf+" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMUw4UHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMUw4kHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMVX8EHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="module_leader(m)=u1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_5q6gwEgCEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMTiwkHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="module_leader ≔ module_leader{m ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.action#_1unQUEHNEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMUw4EHNEeqHd7PiYTbxHg" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMUJ0UHNEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMUJ0kHNEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf/" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="create_programme" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHv">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf," org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHv|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" 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.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="programmes ≔ programmes∪{p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.action#_x9OREEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="programme_leader ≔ programme_leader{p ↦ u}" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.action#_JVrasUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="administrators ≔ administrators∪{p ↦ u}" org.eventb.core.label="act3" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.action#_ROM2IEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_sinpkEHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_gpeM0EgTEeqeqbGZOOBkaQ" org.eventb.core.type="USER"/>
<org.eventb.core.scGuard name="y" org.eventb.core.label="grd51" org.eventb.core.predicate="d∈year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHv|org.eventb.core.guard#_F39EkI8AEeq1J8HIGUp2sw" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="d" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHv|org.eventb.core.parameter#_TsGtoEdGEeqCJoBEKqsuQA" org.eventb.core.type="ℤ"/>
<org.eventb.core.scAction name="z" org.eventb.core.assignment="programme_duration ≔ programme_duration{p ↦ d}" org.eventb.core.label="act52" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHv|org.eventb.core.action#_zUXGUUatEeqCJoBEKqsuQA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf0" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="delete_programme" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf-" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" 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.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" 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.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="programmes ≔ programmes ∖ {p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.action#_3BFMgEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="programme_leader ≔ {p} ⩤ programme_leader" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.action#_g_m5YUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="administrators ≔ {p} ⩤ administrators" org.eventb.core.label="act3" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.action#_g_ngcEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="y" org.eventb.core.assignment="contains_module ≔ {p} ⩤ contains_module" org.eventb.core.label="act21" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj|org.eventb.core.action#_oc4CkEHPEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="z" org.eventb.core.assignment="outcome_mapping ≔ outcome_mapping ⩥ ({p} ◁ ran(outcome_mapping))" org.eventb.core.label="act31" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo|org.eventb.core.action#_oBH5QEmnEeqDwOH5c8gGmw"/>
<org.eventb.core.scAction name="{" org.eventb.core.assignment="programme_outcomes ≔ {p} ⩤ programme_outcomes" org.eventb.core.label="act32" org.eventb.core.source="/progmanmodel/m3_outcomes.bum|org.eventb.core.machineFile#m3_outcomes|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo|org.eventb.core.action#_Mfs94EmiEeqDwOH5c8gGmw"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_3BDXUkHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_oWwBkEgTEeqeqbGZOOBkaQ" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="|" org.eventb.core.assignment="programme_duration ≔ {p} ⩤ programme_duration" org.eventb.core.label="act52" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw|org.eventb.core.action#_l1c0sEauEeqCJoBEKqsuQA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf1" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="add_administrator" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHx">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf." org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHx|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" 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.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" 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.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" 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.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" 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.theorem="false"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="administrators ≔ administrators∪{p ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.action#_7nMcAUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_7nLN4EHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_sinCgEHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_sinCgUHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf2" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="remove_administrator" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHy">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf\/" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHy|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" 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.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" 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.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" 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.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" 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.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" 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.theorem="false"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="administrators ≔ administrators ∖ {p ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.action#_gpmvsUgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_gpmvsEgTEeqeqbGZOOBkaQ" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_3BDXUEHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_3BDXUUHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf3" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="transfer_ownership" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHz">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf0" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHz|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" 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.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" 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.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" 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.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" 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.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" 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.theorem="false"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="programme_leader ≔ programme_leader{p ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.action#_oW2IMUgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_oW2IMEgTEeqeqbGZOOBkaQ" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_7nKm0EHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_7nKm0UHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf4" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="register" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxH{">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf1" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxH{|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="registered ≔ registered∪{u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.action#_eQiycUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_eQiLYEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf5" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unregister" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxH\|">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf2" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxH\||org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scGuard name="w" org.eventb.core.label="grd11" 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.theorem="false"/>
<org.eventb.core.scGuard name="x" org.eventb.core.label="grd12" 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.theorem="false"/>
<org.eventb.core.scGuard name="y" org.eventb.core.label="grd21" org.eventb.core.predicate="u∉ran(module_leader)" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo|org.eventb.core.guard#_mWA5MEHOEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="registered ≔ registered ∖ {u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.action#_eQknoEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_eQjZgEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf6" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="login" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxH}">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf3" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxH}|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="logged_in ≔ logged_in∪{u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.action#_iqZuoUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_iqZHkEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_outcomf7" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="logout" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxH~">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m4_prerequisites.bcm|org.eventb.core.scMachineFile#m4_prerequisites|org.eventb.core.scEvent#programme_outcomf4" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxH~|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="logged_in ≔ logged_in ∖ {u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.action#_iqa8wEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_iqaVsEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>