-
Notifications
You must be signed in to change notification settings - Fork 0
/
secondRef_ctx.bpo
24 lines (24 loc) · 3 KB
/
secondRef_ctx.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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="1">
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="VEHICLE_TYPES" org.eventb.core.type="ℙ(VEHICLE_TYPES)"/>
<org.eventb.core.poIdentifier name="camion_1" org.eventb.core.type="VEHICLE_TYPES"/>
<org.eventb.core.poIdentifier name="camion_2" org.eventb.core.type="VEHICLE_TYPES"/>
<org.eventb.core.poIdentifier name="camion_3" org.eventb.core.type="VEHICLE_TYPES"/>
<org.eventb.core.poIdentifier name="vehicle_slot" org.eventb.core.type="ℙ(VEHICLE_TYPES×ℤ)"/>
<org.eventb.core.poIdentifier name="voiture" org.eventb.core.type="VEHICLE_TYPES"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="axm3/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="1">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/ferryBoat/secondRef_ctx.bpo|org.eventb.core.poFile#secondRef_ctx|org.eventb.core.poPredicateSet#HYP("/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="ran(vehicle_slot)={1,2,3}" org.eventb.core.source="/FerryBoat/secondRef_ctx.buc|org.eventb.core.contextFile#secondRef_ctx|org.eventb.core.axiom#\/"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/FerryBoat/secondRef_ctx.buc|org.eventb.core.contextFile#secondRef_ctx|org.eventb.core.axiom#\/"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/ferryBoat/secondRef_ctx.bpo|org.eventb.core.poFile#secondRef_ctx|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/ferryBoat/secondRef_ctx.bpo|org.eventb.core.poFile#secondRef_ctx|org.eventb.core.poPredicateSet#HYP("/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="HYP(" org.eventb.core.parentSet="/ferryBoat/secondRef_ctx.bpo|org.eventb.core.poFile#secondRef_ctx|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="1">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="partition(VEHICLE_TYPES,{voiture},{camion_1},{camion_2},{camion_3})" org.eventb.core.source="/FerryBoat/secondRef_ctx.buc|org.eventb.core.contextFile#secondRef_ctx|org.eventb.core.axiom#)"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="vehicle_slot={voiture ↦ 1,camion_1 ↦ 1,camion_2 ↦ 2,camion_3 ↦ 3}" org.eventb.core.source="/FerryBoat/secondRef_ctx.buc|org.eventb.core.contextFile#secondRef_ctx|org.eventb.core.axiom#."/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/ferryBoat/secondRef_ctx.bpo|org.eventb.core.poFile#secondRef_ctx|org.eventb.core.poPredicateSet#HYP(" org.eventb.core.poStamp="1">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="ran(vehicle_slot)={1,2,3}" org.eventb.core.source="/FerryBoat/secondRef_ctx.buc|org.eventb.core.contextFile#secondRef_ctx|org.eventb.core.axiom#\/"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>