<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="48">
<org.eventb.core.poIdentifier name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.poIdentifier name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.poIdentifier name="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
<org.eventb.core.poIdentifier name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.poIdentifier name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.poIdentifier name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.poIdentifier name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.poIdentifier name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.poIdentifier name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.axiom#axm1"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.axiom#axm2"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="partition(MINE_SET,{M})" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.axiom#axm3"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="48">
<org.eventb.core.poIdentifier name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.poIdentifier name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.poIdentifier name="methane" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.poIdentifier name="pump" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.poIdentifier name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="inv6/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="dom(pump)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv6"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv6"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="inv7/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV5"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="dom(bell)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv7"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv7"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV5"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="inv8/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV6"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="dom(methane)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv8"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv8"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV6"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="inv9/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV7"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="dom(waterLevel)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv9"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv9"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV7"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="inv10/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV8"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF∧(pump(m)=ON∨(m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF))" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set6"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set6"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV8"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="inv10/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV8"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set6"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set6"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV8"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="inv12/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV10"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(waterLevel(m)=LOW∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(waterLevel(m)=MEDIUM∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL))))" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set8"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set8"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV10"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="inv12/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV10"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set8"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set8"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV10"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv2/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="(∅ ⦂ ℙ(MINE_SET×ONOFF))∈(∅ ⦂ ℙ(MINE_SET)) → ONOFF" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt1"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#INITIALISATION\/inv2\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv3/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="(∅ ⦂ ℙ(MINE_SET×BOOL))∈(∅ ⦂ ℙ(MINE_SET)) → BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv3"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt1"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv3"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#INITIALISATION\/inv3\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv4/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="(∅ ⦂ ℙ(MINE_SET×BOOL))∈(∅ ⦂ ℙ(MINE_SET)) → BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv4"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt1"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv4"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#INITIALISATION\/inv4\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv5/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="(∅ ⦂ ℙ(MINE_SET×LEVEL))∈(∅ ⦂ ℙ(MINE_SET)) → LEVEL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv5"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt1"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv5"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#INITIALISATION\/inv5\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT0" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="48">
<org.eventb.core.poIdentifier name="bell'" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.poIdentifier name="MINE'" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.poIdentifier name="waterLevel'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.poIdentifier name="pump'" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.poIdentifier name="methane'" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT0" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTIDENTEVT0" org.eventb.core.poStamp="48"/>
<org.eventb.core.poSequent name="updatePump/grd2/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF∧(pump(m)=ON∨(m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF))" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.guard#,"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.guard#,"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="updatePump/grd2/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="pump(m)=ON∨pump(m)=OFF" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.guard#,"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.guard#,"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="updatePump/inv2/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT1">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="(pump(m)=OFF∧pump'=pump{m ↦ ON})∨(pump(m)=ON∧pump'=pump{m ↦ OFF})" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.action#+"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="pump'∈MINE → ONOFF" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#updatePump\/inv2\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="updatePump/act1/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of action" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT1"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="∀pump'⦂ℙ(MINE_SET×ONOFF)·m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF∧((pump(m)=OFF∧pump'=pump{m ↦ ON})∨(m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF))" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.action#+"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="updatePump/act1/FIS" org.eventb.core.accurate="true" org.eventb.core.poDesc="Feasibility of action" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT1"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="∃pump'⦂ℙ(MINE_SET×ONOFF)·(pump(m)=OFF∧pump'=pump{m ↦ ON})∨(pump(m)=ON∧pump'=pump{m ↦ OFF})" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.action#+"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT1" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="48">
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.poIdentifier name="pump'" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT1GRD0" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTIDENTEVT1" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.guard#("/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT1" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="pump(m)=ON∨pump(m)=OFF" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt2|org.eventb.core.guard#,"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="updateBell/inv3/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT2"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="bell{m ↦ status}∈MINE → BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv3"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt3"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv3"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#updateBell\/inv3\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT2" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="48">
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.poIdentifier name="status" org.eventb.core.type="BOOL"/>
<org.eventb.core.poIdentifier name="bell'" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT2" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTIDENTEVT2" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt3|org.eventb.core.guard#)"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="status∈BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt3|org.eventb.core.guard#-"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="updateMethane/inv4/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT3"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="methane{m ↦ status}∈MINE → BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv4"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt4"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv4"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#updateMethane\/inv4\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT3" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="48">
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.poIdentifier name="status" org.eventb.core.type="BOOL"/>
<org.eventb.core.poIdentifier name="methane'" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT3" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTIDENTEVT3" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt4|org.eventb.core.guard#)"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="status∈BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt4|org.eventb.core.guard#*"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="updateWaterLevel/grd2/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(waterLevel(m)=LOW∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(waterLevel(m)=MEDIUM∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL))))" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.guard#,"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.guard#,"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="updateWaterLevel/grd2/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.guard#,"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.guard#,"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="updateWaterLevel/inv5/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT4">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.action#+"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="waterLevel'∈MINE → LEVEL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv5"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv5"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#updateWaterLevel\/inv5\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="updateWaterLevel/act1/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of action" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT4"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="∀waterLevel'⦂ℙ(MINE_SET×LEVEL)·m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL))))))" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.action#+"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="updateWaterLevel/act1/FIS" org.eventb.core.accurate="true" org.eventb.core.poDesc="Feasibility of action" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT4"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.action#+"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT4" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="48">
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.poIdentifier name="waterLevel'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT4GRD0" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTIDENTEVT4" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.guard#)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT4" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt5|org.eventb.core.guard#,"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="addMine/inv2/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT5"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="pump{M ↦ OFF}∈{M} → ONOFF" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#addMine\/inv2\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="addMine/inv3/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT5"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="bell{M ↦ FALSE}∈{M} → BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv3"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv3"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#addMine\/inv3\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="addMine/inv4/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT5"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="methane{M ↦ FALSE}∈{M} → BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv4"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv4"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#addMine\/inv4\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="addMine/inv5/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTALLHYPEVT5"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="waterLevel{M ↦ LOW}∈{M} → LEVEL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv5"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv5"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poSequent#addMine\/inv5\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT5" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="48">
<org.eventb.core.poIdentifier name="bell'" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.poIdentifier name="MINE'" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.poIdentifier name="waterLevel'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.poIdentifier name="pump'" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.poIdentifier name="methane'" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT5" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#EVTIDENTEVT5" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="MINE=(∅ ⦂ ℙ(MINE_SET))" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6|org.eventb.core.guard#,"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPINV4" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv1"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="pump∈MINE → ONOFF" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="bell∈MINE → BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv3"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="methane∈MINE → BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv4"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="waterLevel∈MINE → LEVEL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv5"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPINV5" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV4" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="dom(pump)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv6"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPINV6" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV5" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="dom(bell)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv7"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPINV7" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV6" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="dom(methane)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv8"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPINV8" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV7" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD8" org.eventb.core.predicate="dom(waterLevel)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv9"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPINV10" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV8" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD9" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set6"/>
<org.eventb.core.poPredicate name="PRD10" org.eventb.core.predicate="MINE⊆MINE_SET" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set7"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/MinePump.bpo|org.eventb.core.poFile#MinePump|org.eventb.core.poPredicateSet#HYPINV10" org.eventb.core.poStamp="48">
<org.eventb.core.poPredicate name="PRD11" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set8"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>
