<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.prFile version="1">
<org.eventb.core.prProof name="methane_leak/act1/SIM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7" org.eventb.core.prSets="LEVEL,MINE_SET,ONOFF">
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p7,p2,p1,p6,p3,p4,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="methane" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="methane{m ↦ TRUE}=methane{m ↦ TRUE}"/>
</org.eventb.core.prProof>
</org.eventb.core.prFile>
