<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.prFile version="1">
<org.eventb.core.prProof name="inv6/THM" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="p0,p1" org.eventb.core.prSets="LEVEL,ONOFF">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p2,p3"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p2,p3"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p0" org.eventb.core.prInfHyps="p4,p5,p6,p7"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p0"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5,p6,p7"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p8" org.eventb.core.prInfHyps="p9"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p8"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p9"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (ONOFF={ON,OFF})" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p11" org.eventb.core.prInfHyps="p12"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (LEVEL={LOW,MEDIUM,HIGH})" org.eventb.core.prHyps="p4">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p13" org.eventb.core.prInfHyps="p14"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p13"/>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p4"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p2"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<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.prPred name="p6" org.eventb.core.predicate="¬LOW=HIGH"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="waterLevel∈MINE → {LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬LOW=MEDIUM"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="partition(MINE_SET,{M})">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="pump∈MINE → {ON,OFF}">
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="pump" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬MEDIUM=HIGH"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel∈MINE → LEVEL">
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="MINE_SET={M}">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="pump∈MINE → ONOFF">
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="pump" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="inv7/THM" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3" org.eventb.core.prSets="LEVEL,ONOFF">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p6,p7,p8,p9"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p6,p7,p8,p9"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p10" org.eventb.core.prInfHyps="p11"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (dom(pump)=MINE)" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p21">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p13" org.eventb.core.prInfHyps="p14"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p15" org.eventb.core.prInfHyps="p16"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p17" org.eventb.core.prInfHyps="p18"/>
<org.eventb.core.prHypAction name="FORWARD_INF3" org.eventb.core.prHyps="p19" org.eventb.core.prInfHyps="p20"/>
<org.eventb.core.prHypAction name="DESELECT4" org.eventb.core.prHyps="p13,p15,p17,p19"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (ONOFF={ON,OFF})" org.eventb.core.prHyps="p4">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p14" org.eventb.core.prInfHyps="p22"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p14"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (LEVEL={LOW,MEDIUM,HIGH})" org.eventb.core.prHyps="p6">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p20" org.eventb.core.prInfHyps="p23"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p20"/>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p6"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p4"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p2"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.prIdent name="pump" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="methane∈dom(pump) → BOOL">
<org.eventb.core.prIdent name="methane" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="waterLevel∈dom(pump) → {LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="methane∈MINE → BOOL">
<org.eventb.core.prIdent name="methane" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬LOW=HIGH"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="pump∈dom(pump) → ONOFF"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬LOW=MEDIUM"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="bell∈dom(pump) → BOOL"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="partition(MINE_SET,{M})">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="dom(bell)=dom(pump)"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="pump∈dom(pump) → {ON,OFF}"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬MEDIUM=HIGH"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="waterLevel∈dom(pump) → LEVEL">
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="waterLevel∈MINE → LEVEL">
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="MINE_SET={M}">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="inv8/THM" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3" org.eventb.core.prSets="LEVEL,ONOFF">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p6,p7,p8,p9"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p6,p7,p8,p9"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p10" org.eventb.core.prInfHyps="p11"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (dom(pump)=MINE)" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p23">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p13" org.eventb.core.prInfHyps="p14"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p15" org.eventb.core.prInfHyps="p16"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p17" org.eventb.core.prInfHyps="p18"/>
<org.eventb.core.prHypAction name="FORWARD_INF3" org.eventb.core.prHyps="p19" org.eventb.core.prInfHyps="p20"/>
<org.eventb.core.prHypAction name="FORWARD_INF4" org.eventb.core.prHyps="p21" org.eventb.core.prInfHyps="p22"/>
<org.eventb.core.prHypAction name="DESELECT5" org.eventb.core.prHyps="p13,p15,p17,p19,p21"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (ONOFF={ON,OFF})" org.eventb.core.prHyps="p4">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p14" org.eventb.core.prInfHyps="p24"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p14"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (LEVEL={LOW,MEDIUM,HIGH})" org.eventb.core.prHyps="p6">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p20" org.eventb.core.prInfHyps="p25"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p20"/>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p6"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p4"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p2"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<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="methane" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.prIdent name="pump" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.prPred name="p25" org.eventb.core.predicate="waterLevel∈dom(pump) → {LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬LOW=HIGH"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="pump∈dom(pump) → ONOFF"/>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="dom(methane)=dom(pump)"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="bell∈dom(pump) → BOOL">
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="dom(bell)=dom(pump)">
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="bell∈MINE → BOOL">
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬MEDIUM=HIGH"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="waterLevel∈dom(pump) → LEVEL">
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="MINE_SET={M}">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="methane∈dom(pump) → BOOL"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬LOW=MEDIUM"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="partition(MINE_SET,{M})">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="dom(bell)=MINE">
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p24" org.eventb.core.predicate="pump∈dom(pump) → {ON,OFF}"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="waterLevel∈MINE → LEVEL">
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="inv9/THM" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3" org.eventb.core.prSets="LEVEL,ONOFF">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p6,p7,p8,p9"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p6,p7,p8,p9"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p10" org.eventb.core.prInfHyps="p11"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (dom(pump)=MINE)" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p25">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p13" org.eventb.core.prInfHyps="p14"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p15" org.eventb.core.prInfHyps="p16"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p17" org.eventb.core.prInfHyps="p18"/>
<org.eventb.core.prHypAction name="FORWARD_INF3" org.eventb.core.prHyps="p19" org.eventb.core.prInfHyps="p20"/>
<org.eventb.core.prHypAction name="FORWARD_INF4" org.eventb.core.prHyps="p21" org.eventb.core.prInfHyps="p22"/>
<org.eventb.core.prHypAction name="FORWARD_INF5" org.eventb.core.prHyps="p23" org.eventb.core.prInfHyps="p24"/>
<org.eventb.core.prHypAction name="DESELECT6" org.eventb.core.prHyps="p13,p15,p17,p19,p21,p23"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (ONOFF={ON,OFF})" org.eventb.core.prHyps="p4">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p14" org.eventb.core.prInfHyps="p26"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p14"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (LEVEL={LOW,MEDIUM,HIGH})" org.eventb.core.prHyps="p6">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p20" org.eventb.core.prInfHyps="p27"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p20"/>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p6"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p4"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p2"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<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="pump" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p27" org.eventb.core.predicate="waterLevel∈dom(pump) → {LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬LOW=HIGH"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="pump∈dom(pump) → ONOFF"/>
<org.eventb.core.prPred name="p25" org.eventb.core.predicate="dom(waterLevel)=dom(pump)"/>
<org.eventb.core.prPred name="p24" org.eventb.core.predicate="dom(methane)=dom(pump)">
<org.eventb.core.prIdent name="methane" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="bell∈dom(pump) → BOOL">
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="dom(bell)=dom(pump)">
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="bell∈MINE → BOOL">
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="dom(methane)=MINE">
<org.eventb.core.prIdent name="methane" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬MEDIUM=HIGH"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="waterLevel∈dom(pump) → LEVEL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="MINE_SET={M}">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="methane∈dom(pump) → BOOL">
<org.eventb.core.prIdent name="methane" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="methane∈MINE → BOOL">
<org.eventb.core.prIdent name="methane" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬LOW=MEDIUM"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="partition(MINE_SET,{M})">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="dom(bell)=MINE">
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p26" org.eventb.core.predicate="pump∈dom(pump) → {ON,OFF}"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="INITIALISATION/inv2/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1" org.eventb.core.prSets="ONOFF">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p2,p3"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p2,p3"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p4" org.eventb.core.prInfHyps="p5,p6,p7,p8"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p4"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p5,p6,p7,p8"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p9" org.eventb.core.prInfHyps="p10"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p9"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (ONOFF={ON,OFF})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p11">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p2"/>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="¬LOW=MEDIUM">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(MINE_SET,{M})">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="(∅ ⦂ ℙ(MINE_SET×ONOFF))∈(∅ ⦂ ℙ(MINE_SET)) → ONOFF"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬LOW=HIGH">
<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.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬MEDIUM=HIGH">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="(∅ ⦂ ℙ(MINE_SET×ONOFF))∈(∅ ⦂ ℙ(MINE_SET)) → {ON,OFF}"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="MINE_SET={M}">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="INITIALISATION/inv3/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p0" org.eventb.core.prInfHyps="p1,p2"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p0"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p1,p2"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5,p6,p7"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5,p6,p7"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p8" org.eventb.core.prInfHyps="p9"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p8"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p9"/>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</org.eventb.core.prRule>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬LOW=MEDIUM">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬ON=OFF">
<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.prPred>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="partition(MINE_SET,{M})">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="¬LOW=HIGH">
<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.prPred>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="ONOFF={ON,OFF}">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬MEDIUM=HIGH">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="MINE_SET={M}">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="INITIALISATION/inv4/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p0" org.eventb.core.prInfHyps="p1,p2"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p0"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p1,p2"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5,p6,p7"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5,p6,p7"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p8" org.eventb.core.prInfHyps="p9"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p8"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p9"/>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</org.eventb.core.prRule>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬LOW=MEDIUM">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬ON=OFF">
<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.prPred>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="partition(MINE_SET,{M})">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="¬LOW=HIGH">
<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.prPred>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="ONOFF={ON,OFF}">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬MEDIUM=HIGH">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="MINE_SET={M}">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="INITIALISATION/inv5/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1" org.eventb.core.prSets="LEVEL">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p2" org.eventb.core.prInfHyps="p3,p4"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p2"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p3,p4"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p5,p6,p7,p8"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p5,p6,p7,p8"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p9" org.eventb.core.prInfHyps="p10"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p9"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (LEVEL={LOW,MEDIUM,HIGH})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p5">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p11">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="¬LOW=MEDIUM"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="¬ON=OFF">
<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.prPred>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(MINE_SET,{M})">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="(∅ ⦂ ℙ(MINE_SET×LEVEL))∈(∅ ⦂ ℙ(MINE_SET)) → LEVEL"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬LOW=HIGH"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="ONOFF={ON,OFF}">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬MEDIUM=HIGH"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="MINE_SET={M}">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="(∅ ⦂ ℙ(MINE_SET×LEVEL))∈(∅ ⦂ ℙ(MINE_SET)) → {LOW,MEDIUM,HIGH}"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="high_water_detected/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2" org.eventb.core.prSets="LEVEL,MINE_SET">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p2" org.eventb.core.prInfHyps="p6,p7,p8,p9"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p2"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p6,p7,p8,p9"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p10"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (LEVEL={LOW,MEDIUM,HIGH})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p6">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p12">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (MINE_SET={M})" org.eventb.core.prGoal="p12" org.eventb.core.prHyps="p10">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p13">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.conj" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p13" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p14"/>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p15"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p10"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p6"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="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="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬LOW=HIGH"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ {LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬ON=OFF">
<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.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬LOW=MEDIUM"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈{M} ⇸ {LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ONOFF={ON,OFF}">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬MEDIUM=HIGH"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="MINE_SET={M}"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="waterLevel∈{M} ⇸ {LOW,MEDIUM,HIGH}"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="high_water_detected/grd3/WD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2" org.eventb.core.prSets="MINE_SET">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p6" org.eventb.core.prInfHyps="p7,p8,p9,p10"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p7,p8,p9,p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p11"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (waterLevel(m)=HIGH)" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p7" org.eventb.core.prInfHyps="p13"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p9" org.eventb.core.prInfHyps="p14"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p10" org.eventb.core.prInfHyps="p15"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p7,p9,p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (MINE_SET={M})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p11">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p16">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.conj" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p16" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p17"/>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p18"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p11"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p2"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<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.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬LOW=HIGH">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="¬MEDIUM=waterLevel(m)">
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="m∈dom(methane)∧methane∈{M} ⇸ BOOL"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬ON=OFF">
<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.prPred>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬LOW=MEDIUM">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="m∈dom(methane)"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})">
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ONOFF={ON,OFF}">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="¬MEDIUM=HIGH">
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="methane∈{M} ⇸ BOOL"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="¬LOW=waterLevel(m)">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,waterLevel(m)}">
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="MINE_SET={M}"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(methane)∧methane∈MINE_SET ⇸ BOOL"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="high_water_detected/inv2/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3" org.eventb.core.prSets="ONOFF">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p6" org.eventb.core.prInfHyps="p7,p8,p9,p10"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p7,p8,p9,p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p11" org.eventb.core.prInfHyps="p12"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p13"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (waterLevel(m)=HIGH)" org.eventb.core.prHyps="p1">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p7" org.eventb.core.prInfHyps="p14"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p9" org.eventb.core.prInfHyps="p15"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p10" org.eventb.core.prInfHyps="p16"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p7,p9,p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (pump(m)=OFF)" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p4" org.eventb.core.prInfHyps="p17"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p5" org.eventb.core.prInfHyps="p18"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (ONOFF={ON,pump(m)})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p17">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p21">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p19" org.eventb.core.prInfHyps="p20"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p19"/>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p17"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p2"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p1"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="HIGH" 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="pump" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="pump{m ↦ ON}∈MINE → {ON,pump(m)}"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬LOW=HIGH">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="¬MEDIUM=waterLevel(m)">
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="pump(m)=OFF"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="¬ON=pump(m)"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="pump{m ↦ ON}∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬LOW=MEDIUM">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="partition(MINE_SET,{M})">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})">
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="pump∈MINE → {ON,pump(m)}"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="¬MEDIUM=HIGH">
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="ONOFF={ON,pump(m)}"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="¬LOW=waterLevel(m)">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,waterLevel(m)}">
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE_SET={M}">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="high_water_detected/grd4/WD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3" org.eventb.core.prSets="MINE_SET,ONOFF">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p6" org.eventb.core.prInfHyps="p7,p8,p9,p10"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p7,p8,p9,p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p11"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (waterLevel(m)=HIGH)" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p7" org.eventb.core.prInfHyps="p13"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p9" org.eventb.core.prInfHyps="p14"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p10" org.eventb.core.prInfHyps="p15"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p7,p9,p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (ONOFF={ON,OFF})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p4">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p16">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (MINE_SET={M})" org.eventb.core.prGoal="p16" org.eventb.core.prHyps="p11">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p17">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.conj" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p17" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p18"/>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p19"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p11"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p4"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p2"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" 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="pump" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬LOW=HIGH">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="m∈dom(pump)∧pump∈{M} ⇸ {ON,OFF}"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="¬MEDIUM=waterLevel(m)">
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="pump∈{M} ⇸ {ON,OFF}"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="m∈dom(pump)∧pump∈MINE_SET ⇸ {ON,OFF}"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬LOW=MEDIUM">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})">
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="¬MEDIUM=HIGH">
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="¬LOW=waterLevel(m)">
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,waterLevel(m)}">
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="m∈dom(pump)"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="MINE_SET={M}"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="low_water_detected/grd2/WD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2" org.eventb.core.prSets="LEVEL,MINE_SET">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p2" org.eventb.core.prInfHyps="p6,p7,p8,p9"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p2"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p6,p7,p8,p9"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p10"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (LEVEL={LOW,MEDIUM,HIGH})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p6">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p12">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (MINE_SET={M})" org.eventb.core.prGoal="p12" org.eventb.core.prHyps="p10">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p13">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.conj" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p13" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p14"/>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p15"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p10"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p6"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="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="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬LOW=HIGH"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ {LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬ON=OFF">
<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.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬LOW=MEDIUM"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈{M} ⇸ {LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ONOFF={ON,OFF}">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬MEDIUM=HIGH"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})">
<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="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="MINE_SET={M}"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="waterLevel∈{M} ⇸ {LOW,MEDIUM,HIGH}"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="low_water_detected/grd3/WD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3" org.eventb.core.prSets="MINE_SET,ONOFF">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p6" org.eventb.core.prInfHyps="p7,p8,p9,p10"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p7,p8,p9,p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p2" org.eventb.core.prInfHyps="p11"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p2"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (waterLevel(m)=LOW)" org.eventb.core.prHyps="p1">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p7" org.eventb.core.prInfHyps="p13"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p8" org.eventb.core.prInfHyps="p14"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p9" org.eventb.core.prInfHyps="p15"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p7,p8,p9"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (ONOFF={ON,OFF})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p4">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p16">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (MINE_SET={M})" org.eventb.core.prGoal="p16" org.eventb.core.prHyps="p11">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p17">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.conj" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p17" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p18"/>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p19"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p11"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p4"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p1"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" 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="pump" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="¬waterLevel(m)=HIGH">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬LOW=HIGH">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="m∈dom(pump)∧pump∈{M} ⇸ {ON,OFF}"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="pump∈{M} ⇸ {ON,OFF}"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="m∈dom(pump)∧pump∈MINE_SET ⇸ {ON,OFF}"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="¬waterLevel(m)=MEDIUM">
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="waterLevel(m)=LOW"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬LOW=MEDIUM">
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="¬MEDIUM=HIGH">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="LEVEL={waterLevel(m),MEDIUM,HIGH}">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="m∈dom(pump)"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="MINE_SET={M}"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="low_water_detected/inv2/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3" org.eventb.core.prSets="ONOFF">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p3" org.eventb.core.prInfHyps="p4,p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(LEVEL,{LOW},{MEDIUM},{HIGH}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p6" org.eventb.core.prInfHyps="p7,p8,p9,p10"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p7,p8,p9,p10"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(MINE_SET,{M}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p11" org.eventb.core.prInfHyps="p12"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p11"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p13"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (waterLevel(m)=LOW)" org.eventb.core.prHyps="p1">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p7" org.eventb.core.prInfHyps="p14"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p8" org.eventb.core.prInfHyps="p15"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p9" org.eventb.core.prInfHyps="p16"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p7,p8,p9"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (pump(m)=ON)" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p4" org.eventb.core.prInfHyps="p17"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p5" org.eventb.core.prInfHyps="p18"/>
<org.eventb.core.prHypAction name="DESELECT2" org.eventb.core.prHyps="p4,p5"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (ONOFF={pump(m),OFF})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p17">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p21">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p19" org.eventb.core.prInfHyps="p20"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p19"/>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p17"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p2"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p1"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
</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="LOW" 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="pump" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="pump{m ↦ OFF}∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="¬waterLevel(m)=HIGH">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬LOW=HIGH">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="¬waterLevel(m)=MEDIUM">
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="pump{m ↦ OFF}∈MINE → {pump(m),OFF}"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="¬pump(m)=OFF"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="waterLevel(m)=LOW"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="¬LOW=MEDIUM">
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="partition(MINE_SET,{M})">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="pump∈MINE → {pump(m),OFF}"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="¬MEDIUM=HIGH">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="ONOFF={pump(m),OFF}"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)">
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="LEVEL={waterLevel(m),MEDIUM,HIGH}">
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="pump(m)=ON"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE_SET={M}">
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
</org.eventb.core.prFile>
