-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathm1_shafts_context.bpr
112 lines (112 loc) · 8.72 KB
/
m1_shafts_context.bpr
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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.prFile version="1">
<org.eventb.core.prProof name="axm2/WD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="" org.eventb.core.prSets="SHAFTS">
<org.eventb.core.lang name="L"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(SHAFTS,UP,DOWN))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
<org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4"/>
<org.eventb.core.prAnte name="(" org.eventb.core.prGoal="p5"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="DOWN" org.eventb.core.type="ℙ(SHAFTS)"/>
<org.eventb.core.prIdent name="UP" org.eventb.core.type="ℙ(SHAFTS)"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="SHAFTS=UP∪DOWN"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="finite(UP)"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(SHAFTS,UP,DOWN)"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="finite(UP)∧finite(DOWN)"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="UP∩DOWN=(∅ ⦂ ℙ(SHAFTS))"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="finite(DOWN)"/>
<org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.conj:0"/>
<org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="avoid_collisions/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="c" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1" org.eventb.core.prSets="CABINS">
<org.eventb.core.lang name="L"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p2" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p3"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∀ goal (frees c)" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
<org.eventb.core.prIdent name="c" org.eventb.core.type="CABINS"/>
<org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6" org.eventb.core.prHyps="p5">
<org.eventb.core.prRule name="r3" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="functional goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps="p1"/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="FLOORS" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.prIdent name="UP" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(CABIN_FLOOR)⇒CABIN_FLOOR(c)∉ran({c} ⩤ CABIN_FLOOR)">
<org.eventb.core.prIdent name="CABIN_FLOOR" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(UP)⇒UP∈CABINS ⇸ ℤ"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(CABIN_FLOOR)⇒¬CABIN_FLOOR(c)∈ran({c} ⩤ CABIN_FLOOR)">
<org.eventb.core.prIdent name="CABIN_FLOOR" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="c∈dom(UP)⇒UP∈CABINS ⇸ ℤ">
<org.eventb.core.prIdent name="c" org.eventb.core.type="CABINS"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="c∈dom(UP)">
<org.eventb.core.prIdent name="c" org.eventb.core.type="CABINS"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="UP∈CABINS ⇸ ℤ"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="UP∈CABINS → FLOORS"/>
<org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
<org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.allI"/>
<org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.impI"/>
<org.eventb.core.prReas name="r3" org.eventb.core.prRID="org.eventb.core.seqprover.isFunGoal"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="avoid_collisions_2/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="c" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1" org.eventb.core.prSets="CABINS">
<org.eventb.core.lang name="L"/>
<org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'">
<org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p2" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p3"/>
<org.eventb.core.prHypAction name="REWRITE1" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
<org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∀ goal (frees c)" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6">
<org.eventb.core.prIdent name="c" org.eventb.core.type="CABINS"/>
<org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p8" org.eventb.core.prHyps="p7">
<org.eventb.core.prRule name="r3" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="functional goal" org.eventb.core.prGoal="p8" org.eventb.core.prHyps="p1"/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="DOWN" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.prIdent name="FLOORS" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="DOWN∈CABINS → FLOORS"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="c∈dom(DOWN)⇒DOWN∈CABINS ⇸ ℤ">
<org.eventb.core.prIdent name="c" org.eventb.core.type="CABINS"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(CABIN_FLOOR)⇒CABIN_FLOOR(c)∉ran({c} ⩤ CABIN_FLOOR)">
<org.eventb.core.prIdent name="CABIN_FLOOR" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(UP)⇒UP(c)∉ran({c} ⩤ UP)">
<org.eventb.core.prIdent name="UP" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(CABIN_FLOOR)⇒¬CABIN_FLOOR(c)∈ran({c} ⩤ CABIN_FLOOR)">
<org.eventb.core.prIdent name="CABIN_FLOOR" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(UP)⇒¬UP(c)∈ran({c} ⩤ UP)">
<org.eventb.core.prIdent name="UP" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="c∈dom(DOWN)">
<org.eventb.core.prIdent name="c" org.eventb.core.type="CABINS"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(DOWN)⇒DOWN∈CABINS ⇸ ℤ"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="DOWN∈CABINS ⇸ ℤ"/>
<org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
<org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.allI"/>
<org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.impI"/>
<org.eventb.core.prReas name="r3" org.eventb.core.prRID="org.eventb.core.seqprover.isFunGoal"/>
</org.eventb.core.prProof>
</org.eventb.core.prFile>