-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathm0_cabins_context.bpo
44 lines (44 loc) · 7.33 KB
/
m0_cabins_context.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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="CABINS" org.eventb.core.type="ℙ(CABINS)"/>
<org.eventb.core.poIdentifier name="CABIN_FLOOR" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.poIdentifier name="FLOORS" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.poIdentifier name="TOP_FLOOR" org.eventb.core.type="ℤ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="num_floors/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Axiom" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#HYP*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="finite(FLOORS)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MszhAJ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MszhAJ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#HYP*"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="max_num_cabins/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Axiom" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#HYP,"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="finite(CABINS)∧finite(FLOORS)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Rn7VMJ7DEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Rn7VMJ7DEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#HYP,"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="avoid_collisions/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Axiom" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#HYP."/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(CABIN_FLOOR)⇒CABIN_FLOOR∈CABINS ⇸ ℤ" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Ms1WMJ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Ms1WMJ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#HYP."/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="HYP*" org.eventb.core.parentSet="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="TOP_FLOOR∈ℕ1" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MsxEwJ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="TOP_FLOOR=7" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Msxr0J6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="FLOORS=0 ‥ TOP_FLOOR" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MsyS4J6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="finite(CABINS)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_M9xTMJ7DEeqVQ6qy3MLSjQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYP," org.eventb.core.parentSet="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#HYP*" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="card(FLOORS)=TOP_FLOOR+1" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MszhAJ6tEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="finite(FLOORS)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MszhAZ6tEeqVQ6qy3MLSjQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYP." org.eventb.core.parentSet="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#HYP," org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="card(CABINS)<card(FLOORS)∗2" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Rn7VMJ7DEeqVQ6qy3MLSjQ"/>
<org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="CABIN_FLOOR∈CABINS → FLOORS" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Ms0vIJ6tEeqVQ6qy3MLSjQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/MULTI-Elevator/m0_cabins_context.bpo|org.eventb.core.poFile#m0_cabins_context|org.eventb.core.poPredicateSet#HYP." org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD8" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(CABIN_FLOOR)⇒CABIN_FLOOR(c)∉ran({c} ⩤ CABIN_FLOOR)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Ms1WMJ6tEeqVQ6qy3MLSjQ"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>