<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;org.animb.valuation.valBase">
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm1" 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.theorem="false"/>
<org.eventb.core.scAxiom name="AXM1" org.eventb.core.label="axm2" 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.theorem="false"/>
<org.eventb.core.scAxiom name="AXM2" org.eventb.core.label="axm3" 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.theorem="false"/>
<org.eventb.core.scConstant name="HIGH" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst5" org.eventb.core.type="LEVEL"/>
<org.eventb.core.scCarrierSet name="LEVEL" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.carrierSet#set2" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.scConstant name="LOW" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst3" org.eventb.core.type="LEVEL"/>
<org.eventb.core.scConstant name="M" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst6" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scConstant name="MEDIUM" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst4" org.eventb.core.type="LEVEL"/>
<org.eventb.core.scCarrierSet name="MINE_SET" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.carrierSet#set3" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.scConstant name="OFF" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst2" org.eventb.core.type="ONOFF"/>
<org.eventb.core.scConstant name="ON" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst1" org.eventb.core.type="ONOFF"/>
<org.eventb.core.scCarrierSet name="ONOFF" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.carrierSet#set1" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.scContextFile>
