-
Notifications
You must be signed in to change notification settings - Fork 0
/
m6_core.bpo
947 lines (947 loc) · 181 KB
/
m6_core.bpo
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
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
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="25">
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="USER" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.poIdentifier name="PROGRAMME" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="MODULE" org.eventb.core.type="ℙ(MODULE)"/>
<org.eventb.core.poIdentifier name="credits" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.poIdentifier name="sum" org.eventb.core.type="ℙ(ℙ(MODULE×ℤ)×ℤ)"/>
<org.eventb.core.poPredicate name="PROGRAMMF" 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.poPredicate name="PROGRAMMG" 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.poPredicate name="PROGRAMMH" 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.poPredicate name="PROGRAMMI" 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.poIdentifier name="M_OUTCOME" org.eventb.core.type="ℙ(M_OUTCOME)"/>
<org.eventb.core.poIdentifier name="P_OUTCOME" org.eventb.core.type="ℙ(P_OUTCOME)"/>
<org.eventb.core.poIdentifier name="SEMESTER" org.eventb.core.type="ℙ(SEMESTER)"/>
<org.eventb.core.poIdentifier name="YEAR" org.eventb.core.type="ℙ(YEAR)"/>
<org.eventb.core.poIdentifier name="semester" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.poIdentifier name="year" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.poPredicate name="P_OUTCOMF" 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.poPredicate name="P_OUTCOMG" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="administrators" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="contains_module" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="core" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="credits_awarded" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="logged_in" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.poIdentifier name="module_leader" org.eventb.core.type="ℙ(MODULE×USER)"/>
<org.eventb.core.poIdentifier name="module_outcomes" org.eventb.core.type="ℙ(MODULE×M_OUTCOME)"/>
<org.eventb.core.poIdentifier name="module_semester" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="module_year" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="modules" org.eventb.core.type="ℙ(MODULE)"/>
<org.eventb.core.poIdentifier name="outcome_mapping" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
<org.eventb.core.poIdentifier name="prerequisites" org.eventb.core.type="ℙ(MODULE×MODULE)"/>
<org.eventb.core.poIdentifier name="programme_duration" org.eventb.core.type="ℙ(PROGRAMME×ℤ)"/>
<org.eventb.core.poIdentifier name="programme_leader" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="programme_outcomes" org.eventb.core.type="ℙ(PROGRAMME×P_OUTCOME)"/>
<org.eventb.core.poIdentifier name="programmes" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="published" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="registered" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.poPredicate name="programme_outcomet" org.eventb.core.predicate="registered⊆USER" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.invariant#_QUDCYEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="programme_outcomeu" 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.poPredicate name="programme_outcomev" org.eventb.core.predicate="programmes⊆PROGRAMME" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_liiugEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="programme_outcomew" org.eventb.core.predicate="programme_leader∈programmes → registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="programme_outcomex" org.eventb.core.predicate="administrators∈programmes ↔ registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="programme_outcomey" 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.poPredicate name="programme_outcomez" 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.poPredicate name="programme_outcome{" 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.poPredicate name="programme_outcome|" 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.poPredicate name="programme_outcome}" 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.poPredicate name="programme_outcome~" 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.poPredicate name="programme_outcomf'" 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.poPredicate name="programme_outcomf(" 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.poPredicate name="programme_outcomf)" 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.poPredicate name="programme_outcomf*" 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.poPredicate name="programme_outcomf+" 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.poPredicate name="programme_outcomf," 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.poPredicate name="programme_outcomf-" 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.poPredicate name="programme_outcomf." 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.poPredicate name="programme_outcomf/" 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.poPredicate name="programme_outcomf0" 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.poPredicate name="programme_outcomf1" 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.poPredicate name="programme_outcomf2" 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.poPredicateSet>
<org.eventb.core.poSequent name="inv64/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Invariant" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\|"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈published∧y∈year∧s∈semester⇒(core[{p}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\|"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv61/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(PROGRAMME×MODULE))∈(∅ ⦂ ℙ(PROGRAMME)) ↔ (∅ ⦂ ℙ(MODULE))" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#INITIALISATION\/inv61\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv62/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(PROGRAMME×MODULE))⊆(∅ ⦂ ℙ(PROGRAMME×MODULE))" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#INITIALISATION\/inv62\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,m⦂MODULE·p∈(∅ ⦂ ℙ(PROGRAMME))∧m∈(∅ ⦂ ℙ(PROGRAMME×MODULE))[{p}]⇒(∅ ⦂ ℙ(MODULE×MODULE))[{m}]⊆(∅ ⦂ ℙ(PROGRAMME×MODULE))[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#INITIALISATION\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈(∅ ⦂ ℙ(PROGRAMME))∧y∈year∧s∈semester⇒sum(((∅ ⦂ ℙ(PROGRAMME×MODULE))[{p}]∩(∅ ⦂ ℙ(MODULE×ℤ))∼[{y}]∩(∅ ⦂ ℙ(MODULE×ℤ))∼[{s}]) ◁ (∅ ⦂ ℙ(MODULE×ℤ)))≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#INITIALISATION\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomet" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="programmes'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="published'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="programme_outcomes'" org.eventb.core.type="ℙ(PROGRAMME×P_OUTCOME)"/>
<org.eventb.core.poIdentifier name="programme_duration'" org.eventb.core.type="ℙ(PROGRAMME×ℤ)"/>
<org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.poIdentifier name="module_outcomes'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME)"/>
<org.eventb.core.poIdentifier name="module_leader'" org.eventb.core.type="ℙ(MODULE×USER)"/>
<org.eventb.core.poIdentifier name="programme_leader'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="credits_awarded'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="module_semester'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="administrators'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="prerequisites'" org.eventb.core.type="ℙ(MODULE×MODULE)"/>
<org.eventb.core.poIdentifier name="core'" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="module_year'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="outcome_mapping'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
<org.eventb.core.poIdentifier name="modules'" org.eventb.core.type="ℙ(MODULE)"/>
<org.eventb.core.poIdentifier name="contains_module'" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="logged_in'" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomet" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomet" org.eventb.core.poStamp="0"/>
<org.eventb.core.poSequent name="set_core/grd8/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu-"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p1⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p1∈published∧y∈year∧s∈semester⇒((core∪{p ↦ m})[{p1}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_FRWL0I7lEeq1J8HIGUp2sw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_FRWL0I7lEeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu-"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="set_core/inv61/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomeu"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core∪{p ↦ m}∈programmes ↔ modules" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#set_core\/inv61\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="set_core/inv62/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomeu"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core∪{p ↦ m}⊆contains_module" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#set_core\/inv62\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="set_core/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomeu"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,m0⦂MODULE·p0∈published∧m0∈(core∪{p ↦ m})[{p0}]⇒prerequisites[{m0}]⊆(core∪{p ↦ m})[{p0}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#set_core\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="set_core/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomeu"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published∧y∈year∧s∈semester⇒sum(((core∪{p ↦ m})[{p0}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#set_core\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomeu" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.poIdentifier name="core'" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomeu-" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomeu" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_F6LAAkgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_F6LAA0gQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_F6LnEEgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_F6LnEUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="m∈contains_module[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_CkeIIEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="m∉core[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_CkeIIUgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_MZzs8EjAEeqDwOH5c8gGmw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomeu" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu-" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="∀p1⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p1∈published∧y∈year∧s∈semester⇒sum(((core∪{p ↦ m})[{p1}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_F6KY8EgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_FRWL0I7lEeq1J8HIGUp2sw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="set_optional/grd8/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev-"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p1⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p1∈published∧y∈year∧s∈semester⇒((core ∖ {p ↦ m})[{p1}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_AX8XcI7mEeq1J8HIGUp2sw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_AX8XcI7mEeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev-"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="set_optional/inv61/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core ∖ {p ↦ m}∈programmes ↔ modules" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#set_optional\/inv61\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="set_optional/inv62/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core ∖ {p ↦ m}⊆contains_module" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#set_optional\/inv62\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="set_optional/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,m0⦂MODULE·p0∈published∧m0∈(core ∖ {p ↦ m})[{p0}]⇒prerequisites[{m0}]⊆(core ∖ {p ↦ m})[{p0}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#set_optional\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="set_optional/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published∧y∈year∧s∈semester⇒sum(((core ∖ {p ↦ m})[{p0}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#set_optional\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomev" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.poIdentifier name="core'" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomev-" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomev" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_JZJoUEgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_JZJoUUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_JZKPYEgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_JZKPYUgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="m∈contains_module[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_GgLvwEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="m∈core[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_GgLvwUgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_OMWooEjAEeqDwOH5c8gGmw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomev" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev-" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="∀p1⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p1∈published∧y∈year∧s∈semester⇒sum(((core ∖ {p ↦ m})[{p1}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_JZJBQEgQEeqeqbGZOOBkaQ|org.eventb.core.guard#_AX8XcI7mEeq1J8HIGUp2sw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="publish_programme/grd62/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomewz"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀y⦂ℤ,s⦂ℤ,cm⦂ℙ(MODULE)·y∈year∧s∈semester∧cm=core[{p}]∩module_year∼[{y}]∩module_semester∼[{s}]⇒cm ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_Qs8pQEgUEeqeqbGZOOBkaQ|org.eventb.core.guard#_dVbV4FGaEeq01sNmetMbsA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_Qs8pQEgUEeqeqbGZOOBkaQ|org.eventb.core.guard#_dVbV4FGaEeq01sNmetMbsA"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomewz"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="publish_programme/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomew"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,m⦂MODULE·p0∈published∪{p}∧m∈core[{p0}]⇒prerequisites[{m}]⊆core[{p0}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk33wEgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_Qs8pQEgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#publish_programme\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="publish_programme/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomew"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published∪{p}∧y∈year∧s∈semester⇒sum((core[{p0}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk33wEgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_Qs8pQEgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#publish_programme\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomew" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="published'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomewz" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomew" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzoEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzoUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="u=programme_leader(p)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzokHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_sioQokHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicate name="PRD6" 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.poPredicate name="PRD7" org.eventb.core.predicate="∀m⦂MODULE·m∈core[{p}]⇒prerequisites[{m}]⊆core[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_Qs8pQEgUEeqeqbGZOOBkaQ|org.eventb.core.guard#_L5uCMEjBEeqDwOH5c8gGmw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomew" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomewz" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD8" org.eventb.core.predicate="∀y⦂ℤ,s⦂ℤ,cm⦂ℙ(MODULE)·y∈year∧s∈semester∧cm=core[{p}]∩module_year∼[{y}]∩module_semester∼[{s}]⇒sum(cm ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_Qs8pQEgUEeqeqbGZOOBkaQ|org.eventb.core.guard#_dVbV4FGaEeq01sNmetMbsA"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="unpublish_programme/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomex"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,m⦂MODULE·p0∈published ∖ {p}∧m∈core[{p0}]⇒prerequisites[{m}]⊆core[{p0}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk4e0UgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_Qs8pQkgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#unpublish_programme\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="unpublish_programme/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomex"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published ∖ {p}∧y∈year∧s∈semester⇒sum((core[{p0}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk4e0UgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_Qs8pQkgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#unpublish_programme\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomex" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="published'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomex" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomex" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_lrQEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_mSUEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="u=programme_leader(p)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_mSUUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="p∈published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_3BElcEHHEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="change_semester/grd61/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="21">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomey\/"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s1⦂ℤ·p∈published∧y∈year∧s1∈semester⇒(core[{p}]∩module_year∼[{y}]∩(module_semester{m ↦ s})∼[{s1}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi|org.eventb.core.guard#_wSfYwEjGEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi|org.eventb.core.guard#_wSfYwEjGEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomey\/"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_semester/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="21">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomey"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s0⦂ℤ·p∈published∧y∈year∧s0∈semester⇒sum((core[{p}]∩module_year∼[{y}]∩(module_semester{m ↦ s})∼[{s0}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_tmqr0Ec-EeqCJoBEKqsuQA"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#change_semester\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomey" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="s" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="module_semester'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomey/" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomey" org.eventb.core.poStamp="21">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicate name="PRD6" 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.poPredicate name="PRD7" 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.poPredicate name="PRD8" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomey" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomey\/" org.eventb.core.poStamp="21">
<org.eventb.core.poPredicate name="PRD9" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s1⦂ℤ·p∈published∧y∈year∧s1∈semester⇒sum((core[{p}]∩module_year∼[{y}]∩(module_semester{m ↦ s})∼[{s1}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi|org.eventb.core.guard#_wSfYwEjGEeqDwOH5c8gGmw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="change_year/grd61/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="22">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomez2"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y1⦂ℤ,s⦂ℤ·p∈published∧y1∈year∧s∈semester⇒(core[{p}]∩(module_year{m ↦ y})∼[{y1}]∩module_semester∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj|org.eventb.core.guard#_vNBHEI7mEeq1J8HIGUp2sw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj|org.eventb.core.guard#_vNBHEI7mEeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomez2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="22">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomez"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y0⦂ℤ,s⦂ℤ·p∈published∧y0∈year∧s∈semester⇒sum((core[{p}]∩(module_year{m ↦ y})∼[{y0}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1gjcEdBEeqCJoBEKqsuQA"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#change_year\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomez" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="y" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="module_year'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomez2" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomez" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicate name="PRD6" 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.poPredicate name="PRD7" 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.poPredicate name="PRD8" 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.poPredicate name="PRD9" 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.poPredicate name="PRD10" 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.poPredicate name="PRD11" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomez" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomez2" org.eventb.core.poStamp="22">
<org.eventb.core.poPredicate name="PRD12" org.eventb.core.predicate="∀p⦂PROGRAMME,y1⦂ℤ,s⦂ℤ·p∈published∧y1∈year∧s∈semester⇒sum((core[{p}]∩(module_year{m ↦ y})∼[{y1}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj|org.eventb.core.guard#_vNBHEI7mEeq1J8HIGUp2sw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcome{" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="programme_duration'" org.eventb.core.type="ℙ(PROGRAMME×ℤ)"/>
<org.eventb.core.poIdentifier name="d" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcome{" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcome{" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicate name="PRD6" 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.poPredicateSet>
<org.eventb.core.poSequent name="assign_prerequisite/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcome\|"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,m⦂MODULE·p∈published∧m∈core[{p}]⇒(prerequisites∪{m1 ↦ m2})[{m}]⊆core[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHl"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#assign_prerequisite\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcome|" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="m1" org.eventb.core.type="MODULE"/>
<org.eventb.core.poIdentifier name="prerequisites'" org.eventb.core.type="ℙ(MODULE×MODULE)"/>
<org.eventb.core.poIdentifier name="m2" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcome|" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcome\|" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicate name="PRD6" 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.poPredicate name="PRD7" 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.poPredicate name="PRD8" 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.poPredicate name="PRD9" 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.poPredicate name="PRD10" org.eventb.core.predicate="m1∉core[published]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHl|org.eventb.core.guard#_-TAOwI7mEeq1J8HIGUp2sw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="unassign_prerequisite/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcome}"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,m⦂MODULE·p∈published∧m∈core[{p}]⇒(prerequisites ∖ {m1 ↦ m2})[{m}]⊆core[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHm"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#unassign_prerequisite\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcome}" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="m1" org.eventb.core.type="MODULE"/>
<org.eventb.core.poIdentifier name="prerequisites'" org.eventb.core.type="ℙ(MODULE×MODULE)"/>
<org.eventb.core.poIdentifier name="m2" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcome}" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcome}" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcome~" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="programme_outcomes'" org.eventb.core.type="ℙ(PROGRAMME×P_OUTCOME)"/>
<org.eventb.core.poIdentifier name="o" org.eventb.core.type="P_OUTCOME"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcome~" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcome~" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf'" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="programme_outcomes'" org.eventb.core.type="ℙ(PROGRAMME×P_OUTCOME)"/>
<org.eventb.core.poIdentifier name="o" org.eventb.core.type="P_OUTCOME"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.poIdentifier name="outcome_mapping'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf'" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf'" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf(" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="module_outcomes'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME)"/>
<org.eventb.core.poIdentifier name="o" org.eventb.core.type="M_OUTCOME"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf(" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf(" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf)" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="module_outcomes'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME)"/>
<org.eventb.core.poIdentifier name="o" org.eventb.core.type="M_OUTCOME"/>
<org.eventb.core.poIdentifier name="outcome_mapping'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf)" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf)" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf*" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="mo" org.eventb.core.type="M_OUTCOME"/>
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="po" org.eventb.core.type="P_OUTCOME"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.poIdentifier name="outcome_mapping'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf*" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf*" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicate name="PRD6" 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.poPredicate name="PRD7" 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.poPredicate name="PRD8" 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.poPredicate name="PRD9" 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.poPredicate name="PRD10" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf+" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="mo" org.eventb.core.type="M_OUTCOME"/>
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="po" org.eventb.core.type="P_OUTCOME"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.poIdentifier name="outcome_mapping'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf+" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf+" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicate name="PRD6" 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.poPredicate name="PRD7" 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.poPredicate name="PRD8" 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.poPredicate name="PRD9" 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.poPredicate name="PRD10" 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.poPredicateSet>
<org.eventb.core.poSequent name="create_module/grd61/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="23">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf,\|"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y1⦂ℤ,s1⦂ℤ·p∈published∧y1∈year∧s1∈semester⇒(core[{p}]∩(module_year{m ↦ y})∼[{y1}]∩(module_semester{m ↦ s})∼[{s1}]) ◁ (credits_awarded{m ↦ c})∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt|org.eventb.core.guard#_bRohQI7nEeq1J8HIGUp2sw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt|org.eventb.core.guard#_bRohQI7nEeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf,\|"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="create_module/inv61/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="23">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf,"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core∈programmes ↔ modules∪{m}" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#create_module\/inv61\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="create_module/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="23">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf,"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,m0⦂MODULE·p∈published∧m0∈core[{p}]⇒({m} ⩤ prerequisites ⩥ {m})[{m0}]⊆core[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#create_module\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="create_module/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="23">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf,"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y0⦂ℤ,s0⦂ℤ·p∈published∧y0∈year∧s0∈semester⇒sum((core[{p}]∩(module_year{m ↦ y})∼[{y0}]∩(module_semester{m ↦ s})∼[{s0}]) ◁ (credits_awarded{m ↦ c}))≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#create_module\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf," org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="y" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="c" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="module_leader'" org.eventb.core.type="ℙ(MODULE×USER)"/>
<org.eventb.core.poIdentifier name="credits_awarded'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="s" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="module_semester'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="prerequisites'" org.eventb.core.type="ℙ(MODULE×MODULE)"/>
<org.eventb.core.poIdentifier name="module_year'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="modules'" org.eventb.core.type="ℙ(MODULE)"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomf,|" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf," org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicate name="PRD6" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf," org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf,\|" org.eventb.core.poStamp="23">
<org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="∀p⦂PROGRAMME,y1⦂ℤ,s1⦂ℤ·p∈published∧y1∈year∧s1∈semester⇒sum((core[{p}]∩(module_year{m ↦ y})∼[{y1}]∩(module_semester{m ↦ s})∼[{s1}]) ◁ (credits_awarded{m ↦ c}))≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt|org.eventb.core.guard#_bRohQI7nEeq1J8HIGUp2sw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="delete_module/grd61/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="24">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf-}"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈published∧y∈year∧s∈semester⇒((core ⩥ {m})[{p}]∩({m} ⩤ module_year)∼[{y}]∩({m} ⩤ module_semester)∼[{s}]) ◁ ({m} ⩤ credits_awarded)∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu|org.eventb.core.guard#_7vSp8I7oEeq1J8HIGUp2sw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu|org.eventb.core.guard#_7vSp8I7oEeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf-}"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_module/inv61/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="24">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf-"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core ⩥ {m}∈programmes ↔ modules ∖ {m}" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHr"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#delete_module\/inv61\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_module/inv62/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="24">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf-"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core ⩥ {m}⊆contains_module" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHr"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#delete_module\/inv62\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_module/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="24">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf-"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,m0⦂MODULE·p∈published∧m0∈(core ⩥ {m})[{p}]⇒({m} ⩤ prerequisites)[{m0}]⊆(core ⩥ {m})[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHr"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#delete_module\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_module/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="24">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf-"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈published∧y∈year∧s∈semester⇒sum(((core ⩥ {m})[{p}]∩({m} ⩤ module_year)∼[{y}]∩({m} ⩤ module_semester)∼[{s}]) ◁ ({m} ⩤ credits_awarded))≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHr"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#delete_module\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf-" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="module_outcomes'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME)"/>
<org.eventb.core.poIdentifier name="module_leader'" org.eventb.core.type="ℙ(MODULE×USER)"/>
<org.eventb.core.poIdentifier name="credits_awarded'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="module_semester'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="prerequisites'" org.eventb.core.type="ℙ(MODULE×MODULE)"/>
<org.eventb.core.poIdentifier name="core'" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="module_year'" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.poIdentifier name="outcome_mapping'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
<org.eventb.core.poIdentifier name="modules'" org.eventb.core.type="ℙ(MODULE)"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomf-}" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf-" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf-" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf-}" org.eventb.core.poStamp="24">
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈published∧y∈year∧s∈semester⇒sum(((core ⩥ {m})[{p}]∩({m} ⩤ module_year)∼[{y}]∩({m} ⩤ module_semester)∼[{s}]) ◁ ({m} ⩤ credits_awarded))≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu|org.eventb.core.guard#_7vSp8I7oEeq1J8HIGUp2sw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="assign_module/inv62/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="24">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf."/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core⊆contains_module∪{p ↦ m}" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHs"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHv"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#assign_module\/inv62\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf." org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.poIdentifier name="contains_module'" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf." org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf." org.eventb.core.poStamp="24">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicate name="PRD6" 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.poPredicateSet>
<org.eventb.core.poSequent name="unassign_module/inv64/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="25">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf\/x"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p1⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p1∈published∧y∈year∧s∈semester⇒((core ∖ {p ↦ m})[{p1}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw|org.eventb.core.guard#_HKDdEI7pEeq1J8HIGUp2sw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw|org.eventb.core.guard#_HKDdEI7pEeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf\/x"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="unassign_module/inv61/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="25">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf\/"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core ∖ {p ↦ m}∈programmes ↔ modules" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#unassign_module\/inv61\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="unassign_module/inv62/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="25">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf\/"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core ∖ {p ↦ m}⊆contains_module ∖ {p ↦ m}" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#unassign_module\/inv62\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="unassign_module/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="25">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf\/"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,m0⦂MODULE·p0∈published∧m0∈(core ∖ {p ↦ m})[{p0}]⇒prerequisites[{m0}]⊆(core ∖ {p ↦ m})[{p0}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#unassign_module\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="unassign_module/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="25">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf\/"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published∧y∈year∧s∈semester⇒sum(((core ∖ {p ↦ m})[{p0}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#unassign_module\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf/" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.poIdentifier name="core'" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="outcome_mapping'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
<org.eventb.core.poIdentifier name="contains_module'" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomf/x" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf\/" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicate name="PRD6" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf/" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf\/x" org.eventb.core.poStamp="25">
<org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="∀p1⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p1∈published∧y∈year∧s∈semester⇒sum(((core ∖ {p ↦ m})[{p1}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw|org.eventb.core.guard#_HKDdEI7pEeq1J8HIGUp2sw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf0" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u1" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="module_leader'" org.eventb.core.type="ℙ(MODULE×USER)"/>
<org.eventb.core.poIdentifier name="u2" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MODULE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf0" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf0" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicateSet>
<org.eventb.core.poSequent name="create_programme/inv61/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="25">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf1"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="core∈programmes∪{p} ↔ modules" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHv"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHy"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#create_programme\/inv61\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf1" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="programmes'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="programme_duration'" org.eventb.core.type="ℙ(PROGRAMME×ℤ)"/>
<org.eventb.core.poIdentifier name="programme_leader'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="d" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="administrators'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf1" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf1" org.eventb.core.poStamp="25">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sinpkUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="p∈PROGRAMME" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sioQoEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="p∉programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sioQoUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" 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.poPredicateSet>
<org.eventb.core.poSequent name="delete_programme/grd61/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf2*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p1⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p1∈published∧y∈year∧s∈semester⇒(({p} ⩤ core)[{p1}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHz|org.eventb.core.guard#_vWNX8I7pEeq1J8HIGUp2sw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHz|org.eventb.core.guard#_vWNX8I7pEeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf2*"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_programme/inv61/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf2"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{p} ⩤ core∈programmes ∖ {p} ↔ modules" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHz"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#delete_programme\/inv61\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_programme/inv62/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf2"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{p} ⩤ core⊆{p} ⩤ contains_module" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHz"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#delete_programme\/inv62\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_programme/inv63/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf2"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,m⦂MODULE·p0∈published∧m∈({p} ⩤ core)[{p0}]⇒prerequisites[{m}]⊆({p} ⩤ core)[{p0}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHz"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#delete_programme\/inv63\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\||org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_programme/inv64/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf2"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published∧y∈year∧s∈semester⇒sum((({p} ⩤ core)[{p0}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHw"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHz"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poSequent#delete_programme\/inv64\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf2" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="programmes'" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.poIdentifier name="programme_outcomes'" org.eventb.core.type="ℙ(PROGRAMME×P_OUTCOME)"/>
<org.eventb.core.poIdentifier name="programme_duration'" org.eventb.core.type="ℙ(PROGRAMME×ℤ)"/>
<org.eventb.core.poIdentifier name="programme_leader'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="administrators'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.poIdentifier name="core'" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.poIdentifier name="outcome_mapping'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
<org.eventb.core.poIdentifier name="contains_module'" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomf2*" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf2" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="programme_leader(p)=u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YkHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nL08UHHEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf2" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf2*" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="∀p1⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p1∈published∧y∈year∧s∈semester⇒sum((({p} ⩤ core)[{p1}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHz|org.eventb.core.guard#_vWNX8I7pEeq1J8HIGUp2sw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf3" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u1" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="administrators'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="u2" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf3" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf3" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nLN4UHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nLN4kHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nL08EHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gpmIoEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="u2∉administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sio3sEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_cDwN8EHIEeqHd7PiYTbxHg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf4" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u1" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="administrators'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="u2" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf4" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf4" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gpk6gEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gplhkEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gplhkUgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIkgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="u2∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BElcUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_eZxgUEc9EeqCJoBEKqsuQA"/>
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_WXhJ8EgVEeqeqbGZOOBkaQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf5" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u1" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="programme_leader'" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="u2" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="p" org.eventb.core.type="PROGRAMME"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf5" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf5" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW06EEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIUgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_aUM3YEgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="u2∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nMcAEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_bx1dkEgVEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_bx1dkUgVEeqeqbGZOOBkaQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf6" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf6" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf6" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈USER" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQiLYUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u∉registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQiycEHEEeqKzaOTi1o2gg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf7" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf7" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf7" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQjZgUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u∉logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQkAkEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="u∉ran(programme_leader)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj|org.eventb.core.guard#_CWPG4EHIEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="u∉ran(administrators)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj|org.eventb.core.guard#_CWPG4UHIEeqHd7PiYTbxHg"/>
<org.eventb.core.poPredicate name="PRD4" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf8" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="logged_in'" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf8" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf8" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqZHkUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u∉logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqZuoEHEEeqKzaOTi1o2gg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf9" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="19">
<org.eventb.core.poIdentifier name="u" org.eventb.core.type="USER"/>
<org.eventb.core.poIdentifier name="logged_in'" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf9" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf9" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqaVsUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqaVskHEEeqKzaOTi1o2gg"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPc4_prerequisite|" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="core∈programmes ↔ modules" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_yiDSkEgAEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="core⊆contains_module" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_dS7v0EgIEeqeqbGZOOBkaQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="∀p⦂PROGRAMME,m⦂MODULE·p∈published∧m∈core[{p}]⇒prerequisites[{m}]⊆core[{p}]" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_H6Ag0EjAEeqDwOH5c8gGmw"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/progmanmodel/m6_core.bpo|org.eventb.core.poFile#m6_core|org.eventb.core.poPredicateSet#HYPc4_prerequisite\|" org.eventb.core.poStamp="19">
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈published∧y∈year∧s∈semester⇒sum((core[{p}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded)≤60" org.eventb.core.source="/progmanmodel/m6_core.bum|org.eventb.core.machineFile#m6_core|org.eventb.core.invariant#_5Fg8EE5BEeqUxct8tLY9IA"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>