-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathm5_semesters.bpo
983 lines (983 loc) · 192 KB
/
m5_semesters.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
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="11">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="administrators" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.poIdentifier name="contains_module" 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.poPredicateSet>
<org.eventb.core.poSequent name="inv54/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Invariant" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆modules∧m2∈prerequisites[{m1}]⇒m1∈dom(module_year)∧module_year∈MODULE ⇸ ℤ∧m2∈dom(module_year)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="inv55/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Invariant" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitew"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·({m1,m2}⊆modules∧m2∈prerequisites[{m1}]⇒m1∈dom(module_year)∧module_year∈MODULE ⇸ ℤ∧m2∈dom(module_year))∧({m1,m2}⊆modules∧m2∈prerequisites[{m1}]∧module_year(m1)=module_year(m2)⇒m1∈dom(module_semester)∧module_semester∈MODULE ⇸ ℤ∧m2∈dom(module_semester))" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitew"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="inv56/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Invariant" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitex"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈published∧s∈semester∧y∈year⇒(contains_module[{p}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitex"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv51/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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(PROGRAMME×ℤ))∈(∅ ⦂ ℙ(PROGRAMME)) → year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxkkJ6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxkkJ6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#INITIALISATION\/inv51\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv52/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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(MODULE×ℤ))∈(∅ ⦂ ℙ(MODULE)) → semester" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxk0J6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxk0J6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#INITIALISATION\/inv52\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv53/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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(MODULE×ℤ))∈(∅ ⦂ ℙ(MODULE)) → year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_Zoo9wEanEeqCJoBEKqsuQA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_Zoo9wEanEeqCJoBEKqsuQA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#INITIALISATION\/inv53\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv54/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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆(∅ ⦂ ℙ(MODULE))∧m2∈(∅ ⦂ ℙ(MODULE×MODULE))[{m1}]⇒(∅ ⦂ ℙ(MODULE×ℤ))(m1)≥(∅ ⦂ ℙ(MODULE×ℤ))(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#INITIALISATION\/inv54\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitew|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv55/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆(∅ ⦂ ℙ(MODULE))∧m2∈(∅ ⦂ ℙ(MODULE×MODULE))[{m1}]∧(∅ ⦂ ℙ(MODULE×ℤ))(m1)=(∅ ⦂ ℙ(MODULE×ℤ))(m2)⇒(∅ ⦂ ℙ(MODULE×ℤ))(m1)>(∅ ⦂ ℙ(MODULE×ℤ))(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#INITIALISATION\/inv55\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitex|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv56/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomet"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈(∅ ⦂ ℙ(PROGRAMME))∧s∈semester∧y∈year⇒sum(((∅ ⦂ ℙ(PROGRAMME×MODULE))[{p}]∩(∅ ⦂ ℙ(MODULE×ℤ))∼[{y}]∩(∅ ⦂ ℙ(MODULE×ℤ))∼[{s}]) ◁ (∅ ⦂ ℙ(MODULE×ℤ)))≥30" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#INITIALISATION\/inv56\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomet" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|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="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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomet" org.eventb.core.poStamp="0"/>
<org.eventb.core.poSequent name="change_semester/grd4/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu)"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="m∈dom(module_leader)∧module_leader∈MODULE ⇸ USER" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu)"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_semester/grd5/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="m∈dom(module_semester)∧module_semester∈MODULE ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu*"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_semester/grd6/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu+"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m2⦂MODULE·(m2∈modules∧m2∈prerequisites[{m}]⇒m∈dom(module_year)∧module_year∈MODULE ⇸ ℤ∧m2∈dom(module_year))∧(m2∈modules∧m2∈prerequisites[{m}]∧module_year(m)=module_year(m2)⇒m2∈dom(module_semester)∧module_semester∈MODULE ⇸ ℤ)" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu+"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_semester/grd7/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu,"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m2⦂MODULE·(m2∈modules∧m∈prerequisites[{m2}]⇒m∈dom(module_year)∧module_year∈MODULE ⇸ ℤ∧m2∈dom(module_year))∧(m2∈modules∧m∈prerequisites[{m2}]∧module_year(m)=module_year(m2)⇒m2∈dom(module_semester)∧module_semester∈MODULE ⇸ ℤ)" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu,"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_semester/grd9/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="7">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu."/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s1⦂ℤ·p∈published∧s1∈semester∧y∈year⇒(contains_module[{p}]∩module_year∼[{y}]∩(module_semester{m ↦ s})∼[{s1}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu."/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_semester/inv52/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="7">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomeu"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="module_semester{m ↦ s}∈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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxk0J6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#change_semester\/inv52\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_semester/inv55/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="7">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomeu"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆modules∧m2∈prerequisites[{m1}]∧module_year(m1)=module_year(m2)⇒(module_semester{m ↦ s})(m1)>(module_semester{m ↦ s})(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#change_semester\/inv55\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitex|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_semester/inv56/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="7">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomeu"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s0⦂ℤ·p∈published∧s0∈semester∧y∈year⇒sum((contains_module[{p}]∩module_year∼[{y}]∩(module_semester{m ↦ s})∼[{s0}]) ◁ 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#change_semester\/inv56\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomeu" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomeu)" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomeu" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomeu*" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu)" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomeu+" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu*" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomeu," org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu+" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomeu." org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu," org.eventb.core.poStamp="0">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomeu" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomeu." org.eventb.core.poStamp="7">
<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.poSequent name="change_year/grd4/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev)"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="m∈dom(module_leader)∧module_leader∈MODULE ⇸ USER" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev)"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/grd5/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="m∈dom(module_year)∧module_year∈MODULE ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev*"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/grd6/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev+"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m2⦂MODULE·m2∈modules∧m2∈prerequisites[{m}]⇒m2∈dom(module_year)∧module_year∈MODULE ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev+"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/grd7/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev,"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m2⦂MODULE·m2∈modules∧m∈prerequisites[{m2}]⇒m2∈dom(module_year)∧module_year∈MODULE ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev,"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/grd8/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev-"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m2⦂MODULE·(m2∈modules∧m2∈prerequisites[{m}]⇒m2∈dom(module_year)∧module_year∈MODULE ⇸ ℤ)∧(m2∈modules∧m2∈prerequisites[{m}]∧y=module_year(m2)⇒m∈dom(module_semester)∧module_semester∈MODULE ⇸ ℤ∧m2∈dom(module_semester))" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev-"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/grd9/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev."/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m2⦂MODULE·(m2∈modules∧m∈prerequisites[{m2}]⇒m2∈dom(module_year)∧module_year∈MODULE ⇸ ℤ)∧(m2∈modules∧m∈prerequisites[{m2}]∧y=module_year(m2)⇒m∈dom(module_semester)∧module_semester∈MODULE ⇸ ℤ∧m2∈dom(module_semester))" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev."/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/grd12/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev1"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y1⦂ℤ,s⦂ℤ·p∈published∧s∈semester∧y1∈year⇒(contains_module[{p}]∩(module_year{m ↦ y})∼[{y1}]∩module_semester∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/inv53/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="module_year{m ↦ y}∈modules → year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_Zoo9wEanEeqCJoBEKqsuQA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_Zoo9wEanEeqCJoBEKqsuQA"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#change_year\/inv53\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/inv54/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆modules∧m2∈prerequisites[{m1}]⇒(module_year{m ↦ y})(m1)≥(module_year{m ↦ y})(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#change_year\/inv54\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitew|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/inv55/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆modules∧m2∈prerequisites[{m1}]∧(module_year{m ↦ y})(m1)=(module_year{m ↦ y})(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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#change_year\/inv55\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitex|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_year/inv56/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomev"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y0⦂ℤ,s⦂ℤ·p∈published∧s∈semester∧y0∈year⇒sum((contains_module[{p}]∩(module_year{m ↦ y})∼[{y0}]∩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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#change_year\/inv56\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomev" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomev)" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomev" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomev*" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev)" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomev+" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev*" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomev," org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev+" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomev-" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev," org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomev." org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev-" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomev1" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev." org.eventb.core.poStamp="0">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomev" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomev1" org.eventb.core.poStamp="8">
<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.poSequent name="change_duration/grd5/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomew*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="p∈dom(programme_duration)∧programme_duration∈PROGRAMME ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomew*"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="change_duration/inv51/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomew"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="programme_duration{p ↦ d}∈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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_x1iYoEdBEeqCJoBEKqsuQA"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxkkJ6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#change_duration\/inv51\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomew" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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="EVTHYPprogramme_outcomew*" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomew" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomew" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomew*" org.eventb.core.poStamp="5">
<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="publish_programme/grd51/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomexx"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀y⦂ℤ,s⦂ℤ·s∈semester∧y∈year⇒(contains_module[{p}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomexx"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="publish_programme/inv56/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomex"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published∪{p}∧s∈semester∧y∈year⇒sum((contains_module[{p0}]∩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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_EVzGYEgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk33wEgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#publish_programme\/inv56\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomex" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomexx" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomex" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomex" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomexx" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poSequent name="unpublish_programme/inv56/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomey"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published ∖ {p}∧s∈semester∧y∈year⇒sum((contains_module[{p0}]∩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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_EVzGYkgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.event#_Kk4e0UgUEeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#unpublish_programme\/inv56\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomey" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomey" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomey" org.eventb.core.poStamp="5">
<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="assign_prerequisite/grd51/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomez."/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="m2∈dom(module_year)∧module_year∈MODULE ⇸ ℤ∧m1∈dom(module_year)" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomez."/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="assign_prerequisite/grd52/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomezm4"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="m2∈dom(module_year)∧module_year∈MODULE ⇸ ℤ∧m1∈dom(module_year)∧(module_year(m2)=module_year(m1)⇒m2∈dom(module_semester)∧module_semester∈MODULE ⇸ ℤ∧m1∈dom(module_semester))" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomezm4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="assign_prerequisite/inv54/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomez"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m3⦂MODULE,m4⦂MODULE·{m3,m4}⊆modules∧m4∈(prerequisites∪{m1 ↦ m2})[{m3}]⇒module_year(m3)≥module_year(m4)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#assign_prerequisite\/inv54\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitew|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="assign_prerequisite/inv55/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomez"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m3⦂MODULE,m4⦂MODULE·{m3,m4}⊆modules∧m4∈(prerequisites∪{m1 ↦ m2})[{m3}]∧module_year(m3)=module_year(m4)⇒module_semester(m3)>module_semester(m4)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-LeYEJzEeqHCPZ-G665YQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#assign_prerequisite\/inv55\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitex|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomez" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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="EVTHYPprogramme_outcomez." org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomez" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPprogramme_outcomezm4" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomez." org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomez" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomezm4" org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poSequent name="unassign_prerequisite/inv54/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcome{"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m3⦂MODULE,m4⦂MODULE·{m3,m4}⊆modules∧m4∈(prerequisites ∖ {m1 ↦ m2})[{m3}]⇒module_year(m3)≥module_year(m4)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#unassign_prerequisite\/inv54\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitew|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="unassign_prerequisite/inv55/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcome{"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m3⦂MODULE,m4⦂MODULE·{m3,m4}⊆modules∧m4∈(prerequisites ∖ {m1 ↦ m2})[{m3}]∧module_year(m3)=module_year(m4)⇒module_semester(m3)>module_semester(m4)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_D-MFcEJzEeqHCPZ-G665YQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#unassign_prerequisite\/inv55\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitex|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcome{" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcome{" org.eventb.core.poStamp="5">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcome\|" org.eventb.core.poStamp="5">
<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_outcome}" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcome}" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcome}" org.eventb.core.poStamp="5">
<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_outcome~" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcome~" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcome~" org.eventb.core.poStamp="5">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf'" org.eventb.core.poStamp="5">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf(" org.eventb.core.poStamp="5">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf)" org.eventb.core.poStamp="5">
<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/grd53/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="9">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf*{"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y1⦂ℤ,s1⦂ℤ·p∈published∧s1∈semester∧y1∈year⇒(contains_module[{p}]∩(module_year{m ↦ y})∼[{y1}]∩(module_semester{m ↦ s})∼[{s1}]) ◁ (credits_awarded{m ↦ c})∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf*{"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="create_module/inv52/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="9">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="module_semester{m ↦ s}∈modules∪{m} → semester" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxk0J6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxk0J6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#create_module\/inv52\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="create_module/inv53/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="9">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="module_year{m ↦ y}∈modules∪{m} → year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_Zoo9wEanEeqCJoBEKqsuQA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_Zoo9wEanEeqCJoBEKqsuQA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#create_module\/inv53\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="create_module/inv54/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="9">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆modules∪{m}∧m2∈({m} ⩤ prerequisites ⩥ {m})[{m1}]⇒(module_year{m ↦ y})(m1)≥(module_year{m ↦ y})(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#create_module\/inv54\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitew|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="create_module/inv55/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="9">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆modules∪{m}∧m2∈({m} ⩤ prerequisites ⩥ {m})[{m1}]∧(module_year{m ↦ y})(m1)=(module_year{m ↦ y})(m2)⇒(module_semester{m ↦ s})(m1)>(module_semester{m ↦ s})(m2)" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#create_module\/inv55\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitex|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="create_module/inv56/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="9">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y0⦂ℤ,s0⦂ℤ·p∈published∧s0∈semester∧y0∈year⇒sum((contains_module[{p}]∩(module_year{m ↦ y})∼[{y0}]∩(module_semester{m ↦ s})∼[{s0}]) ◁ (credits_awarded{m ↦ c}))≥30" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#create_module\/inv56\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf*" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf*" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf*{" org.eventb.core.poStamp="9">
<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.poSequent name="delete_module/grd51/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="10">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf+{"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p∈published∧s∈semester∧y∈year⇒(contains_module[{p}]∩({m} ⩤ module_year)∼[{y}]∩({m} ⩤ module_semester)∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf+{"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_module/inv52/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="10">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf+"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{m} ⩤ module_semester∈modules ∖ {m} → semester" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxk0J6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxk0J6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#delete_module\/inv52\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_module/inv53/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="10">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf+"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{m} ⩤ module_year∈modules ∖ {m} → year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_Zoo9wEanEeqCJoBEKqsuQA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_Zoo9wEanEeqCJoBEKqsuQA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#delete_module\/inv53\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_module/inv54/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="10">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf+"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆modules ∖ {m}∧m2∈({m} ⩤ prerequisites)[{m1}]⇒({m} ⩤ module_year)(m1)≥({m} ⩤ 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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_TJxqgEg0EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#delete_module\/inv54\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitew|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_module/inv55/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="10">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf+"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m1⦂MODULE,m2⦂MODULE·{m1,m2}⊆modules ∖ {m}∧m2∈({m} ⩤ prerequisites)[{m1}]∧({m} ⩤ module_year)(m1)=({m} ⩤ module_year)(m2)⇒({m} ⩤ module_semester)(m1)>({m} ⩤ 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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_CWrO0Eg2EeqeqbGZOOBkaQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#delete_module\/inv55\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitex|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_module/inv56/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="10">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf+"/>
<org.eventb.core.poPredicate name="SEQHYQ" 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}]) ◁ ({m} ⩤ 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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#delete_module\/inv56\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf+" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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="outcome_mapping'" org.eventb.core.type="ℙ(MODULE×M_OUTCOME×(PROGRAMME×P_OUTCOME))"/>
<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/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf+" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf+{" org.eventb.core.poStamp="10">
<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.poSequent name="assign_module/grd51/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="10">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf,,"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="m∈dom(module_year)∧module_year∈MODULE ⇸ ℤ∧p∈dom(programme_duration)∧programme_duration∈PROGRAMME ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf,,"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="assign_module/inv56/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="10">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf,"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published∧s∈semester∧y∈year⇒sum(((contains_module∪{p ↦ m})[{p0}]∩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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#assign_module\/inv56\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf," org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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="EVTHYPprogramme_outcomf,," org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf," org.eventb.core.poStamp="5">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf," org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf,," org.eventb.core.poStamp="10">
<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/grd51/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="11">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf-,"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p1⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p1∈published∧s∈semester∧y∈year⇒((contains_module ∖ {p ↦ m})[{p1}]∩module_year∼[{y}]∩module_semester∼[{s}]) ◁ credits_awarded∈dom(sum)∧sum∈ℙ(MODULE × ℤ) ⇸ ℤ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf-,"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="unassign_module/inv56/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="11">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf-"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published∧s∈semester∧y∈year⇒sum(((contains_module ∖ {p ↦ m})[{p0}]∩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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHr"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#unassign_module\/inv56\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf-" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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="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-," org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPprogramme_outcomf-" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTHYPprogramme_outcomf-," org.eventb.core.poStamp="11">
<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="EVTIDENTprogramme_outcomf." org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomf." org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf." org.eventb.core.poStamp="5">
<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/inv51/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="11">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf\/"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="programme_duration{p ↦ d}∈programmes∪{p} → year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxkkJ6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHt"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxkkJ6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#create_programme\/inv51\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf/" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomf/" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf\/" org.eventb.core.poStamp="11">
<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/inv51/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf0"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{p} ⩤ programme_duration∈programmes ∖ {p} → year" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxkkJ6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_cOgxkkJ6EeqHCPZ-G665YQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#delete_programme\/inv51\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="delete_programme/inv56/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTALLHYPprogramme_outcomf0"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀p0⦂PROGRAMME,y⦂ℤ,s⦂ℤ·p0∈published∧s∈semester∧y∈year⇒sum((({p} ⩤ contains_module)[{p0}]∩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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/progmanmodel/m4_prerequisites.bum|org.eventb.core.machineFile#m4_prerequisites|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHu"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/progmanmodel/m5_semesters.bum|org.eventb.core.machineFile#m5_semesters|org.eventb.core.invariant#_G6aZYI77Eeq1J8HIGUp2sw"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poSequent#delete_programme\/inv56\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTprogramme_outcomf0" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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="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="EVTALLHYPprogramme_outcomf0" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf0" org.eventb.core.poStamp="5">
<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="EVTIDENTprogramme_outcomf1" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomf1" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf1" org.eventb.core.poStamp="5">
<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_outcomf2" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomf2" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf2" org.eventb.core.poStamp="5">
<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_outcomf3" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomf3" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf3" org.eventb.core.poStamp="5">
<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_outcomf4" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomf4" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf4" org.eventb.core.poStamp="5">
<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_outcomf5" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomf5" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf5" org.eventb.core.poStamp="5">
<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_outcomf6" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomf6" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf6" org.eventb.core.poStamp="5">
<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_outcomf7" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="5">
<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_outcomf7" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#EVTIDENTprogramme_outcomf7" org.eventb.core.poStamp="5">
<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_prerequisitev" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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="PRD1" 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="PRD2" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPc4_prerequisitew" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitev" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD3" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPc4_prerequisitex" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitew" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD4" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/progmanmodel/m5_semesters.bpo|org.eventb.core.poFile#m5_semesters|org.eventb.core.poPredicateSet#HYPc4_prerequisitex" org.eventb.core.poStamp="5">
<org.eventb.core.poPredicate name="PRD5" 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.poFile>