<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.prFile version="1">
<org.eventb.core.prProof name="MinePump_inv9/THM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5" org.eventb.core.prSets="LEVEL,MINE_SET,ONOFF">
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p5,p2,p1,p3,p4">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="INITIALISATION/MinePump_inv5/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3" org.eventb.core.prSets="LEVEL,MINE_SET,ONOFF">
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p3,p2,p1">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="(∅ ⦂ ℙ(MINE_SET×LEVEL))∈(∅ ⦂ ℙ(MINE_SET)) → LEVEL"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="updateWaterLevel/grd2/WD" org.eventb.core.confidence="1000" 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.psManual="true">
<org.eventb.core.prRule name="org.eventb.core.seqprover.disjToImplRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∨ to ⇒ in goal" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p3">
<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="p4"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.totalDom:2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="total function dom substitution in goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p1" org.eventb.core.prHyps="p1"/>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue="1"/>
<org.eventb.core.prExprRef name=".subst" org.eventb.core.prRef="e0"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p5">
<org.eventb.core.prRule name="org.eventb.core.seqprover.isFunGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="functional goal" org.eventb.core.prGoal="p5" org.eventb.core.prHyps="p2"/>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="2" org.eventb.core.prGoal="p6">
<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="p4"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.impI" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p8" org.eventb.core.prHyps="p7">
<org.eventb.core.prRule name="org.eventb.core.seqprover.conj" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p8" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p3">
<org.eventb.core.prRule name="org.eventb.core.seqprover.totalDom:2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="total function dom substitution in goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p1" org.eventb.core.prHyps="p1"/>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue="1"/>
<org.eventb.core.prExprRef name=".subst" org.eventb.core.prRef="e0"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p5">
<org.eventb.core.prRule name="org.eventb.core.seqprover.isFunGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="functional goal" org.eventb.core.prGoal="p5" org.eventb.core.prHyps="p2"/>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="2" org.eventb.core.prGoal="p9">
<org.eventb.core.prRule name="org.eventb.core.seqprover.impI" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p9" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p11" org.eventb.core.prHyps="p10">
<org.eventb.core.prRule name="org.eventb.core.seqprover.conj" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p11" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p3">
<org.eventb.core.prRule name="org.eventb.core.seqprover.totalDom:2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="total function dom substitution in goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps="p2">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p1" org.eventb.core.prHyps="p1"/>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue="1"/>
<org.eventb.core.prExprRef name=".subst" org.eventb.core.prRef="e0"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p5">
<org.eventb.core.prRule name="org.eventb.core.seqprover.isFunGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="functional goal" org.eventb.core.prGoal="p5" org.eventb.core.prHyps="p2"/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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="2"/>
</org.eventb.core.prRule>
<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="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="p11" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="¬waterLevel(m)=LOW⇒m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(¬waterLevel(m)=MEDIUM⇒m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="¬waterLevel(m)=LOW"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="¬waterLevel(m)=MEDIUM"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="¬waterLevel(m)=MEDIUM⇒m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(¬waterLevel(m)=MEDIUM⇒m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(waterLevel(m)=LOW∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(waterLevel(m)=MEDIUM∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL))))"/>
<org.eventb.core.prExpr name="e0" org.eventb.core.expression="MINE"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="updateWaterLevel/grd2/THM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10" org.eventb.core.prSets="LEVEL,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="p10" org.eventb.core.prInfHyps="p11,p12"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p11,p12"/>
<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="p13,p14,p15,p16"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p13,p14,p15,p16"/>
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p6,p9,p4,p5,p2,p8,p7,p11,p12,p13,p14,p15,p16">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</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="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="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="¬LOW=HIGH"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="¬LOW=MEDIUM"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="¬MEDIUM=HIGH"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="waterLevel(m)=LOW∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(waterLevel(m)=MEDIUM∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="updateWaterLevel/MinePump_inv5/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12" org.eventb.core.prSets="LEVEL,MINE_SET,ONOFF" org.eventb.core.psManual="true">
<org.eventb.core.prRule name="org.eventb.core.seqprover.disjE" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∨ hyp (waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH)" org.eventb.core.prHyps="p7">
<org.eventb.core.prAnte name="0" org.eventb.core.prHyps="p13">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p7"/>
<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="p14"/>
<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="p13">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p4" org.eventb.core.prInfHyps="p15"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p4"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p15" org.eventb.core.prInfHyps="p16"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p15"/>
<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="p12" org.eventb.core.prInfHyps="p17,p18"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p17,p18"/>
<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="p19,p20,p21,p22"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p19,p20,p21,p22"/>
<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="p23"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p23"/>
<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="p13">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p19" org.eventb.core.prInfHyps="p24"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p20" org.eventb.core.prInfHyps="p25"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p21" org.eventb.core.prInfHyps="p26"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p19,p20,p21"/>
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p9,p5,p6,p7,p2,p10,p8,p4,p11,p13,p16,p17,p18,p19,p20,p21,p22,p23,p24,p25,p26">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p13"/>
</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.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p13"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prHyps="p27">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="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(ONOFF,{ON},{OFF}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p12" org.eventb.core.prInfHyps="p17,p18"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p17,p18"/>
<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="p19,p20,p21,p22"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p19,p20,p21,p22"/>
<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="p23"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p23"/>
<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="p14"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (waterLevel(m)=MEDIUM)" org.eventb.core.prHyps="p27">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p4" org.eventb.core.prInfHyps="p28"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p19" org.eventb.core.prInfHyps="p29"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p20" org.eventb.core.prInfHyps="p30"/>
<org.eventb.core.prHypAction name="FORWARD_INF3" org.eventb.core.prHyps="p22" org.eventb.core.prInfHyps="p26"/>
<org.eventb.core.prHypAction name="DESELECT4" org.eventb.core.prHyps="p4,p19,p20,p22"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p28" org.eventb.core.prInfHyps="p31"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p28"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (LEVEL={LOW,waterLevel(m),HIGH})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p29">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p33">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p9" org.eventb.core.prInfHyps="p32"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p9"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.disjE" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∨ hyp ((waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ waterLevel(m)})∨waterLevel'=waterLevel{m ↦ LOW}∨waterLevel'=waterLevel{m ↦ HIGH}∨(waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ waterLevel(m)}))" org.eventb.core.prHyps="p31">
<org.eventb.core.prAnte name="0" org.eventb.core.prHyps="p34,p35">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p31"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.contrHyps" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ct in hyps (¬waterLevel(m)=HIGH)" org.eventb.core.prGoal="p33" org.eventb.core.prHyps="p26"/>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prHyps="p36">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p31"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (waterLevel'=waterLevel{m ↦ LOW})" org.eventb.core.prGoal="p33" org.eventb.core.prHyps="p36">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p37">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p37" org.eventb.core.prHyps="p9,p5,p6,p7,p2,p10,p8,p4,p11,p27,p17,p18,p19,p20,p21,p22,p23,p29,p30,p26,p31,p32,p36">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p36"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="2" org.eventb.core.prHyps="p38">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p31"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (waterLevel'=waterLevel{m ↦ HIGH})" org.eventb.core.prGoal="p33" org.eventb.core.prHyps="p38">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p39">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p39" org.eventb.core.prHyps="p9,p5,p6,p7,p2,p10,p8,p4,p11,p27,p17,p18,p19,p20,p21,p22,p23,p29,p30,p26,p31,p32,p38">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p38"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="3" org.eventb.core.prHyps="p13,p35">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p31"/>
<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.prGoal="p33" org.eventb.core.prHyps="p13">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p41">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p30" org.eventb.core.prInfHyps="p40"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p29,p30,p32"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p41" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p43">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p40" org.eventb.core.prInfHyps="p42"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p40"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.falseHyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊥ hyp" org.eventb.core.prHyps="p42"/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p13"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p29"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p27"/>
</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.prAnte>
<org.eventb.core.prAnte name="2" org.eventb.core.prHyps="p34">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p7"/>
<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="p14"/>
<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="p34">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p4" org.eventb.core.prInfHyps="p44"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p4"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p44" org.eventb.core.prInfHyps="p45"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p44"/>
<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="p12" org.eventb.core.prInfHyps="p17,p18"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p12"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p17,p18"/>
<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="p19,p20,p21,p22"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p19,p20,p21,p22"/>
<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="p23"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p23"/>
<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="p34">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p19" org.eventb.core.prInfHyps="p46"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p21" org.eventb.core.prInfHyps="p30"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p22" org.eventb.core.prInfHyps="p47"/>
<org.eventb.core.prHypAction name="DESELECT3" org.eventb.core.prHyps="p19,p21,p22"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (LEVEL={LOW,MEDIUM,waterLevel(m)})" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p46">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p49">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p9" org.eventb.core.prInfHyps="p48"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p9"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.disjE" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∨ hyp (waterLevel'=waterLevel{m ↦ MEDIUM}∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ waterLevel(m)})∨(waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM}))" org.eventb.core.prHyps="p45">
<org.eventb.core.prAnte name="0" org.eventb.core.prHyps="p50">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p45"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.eq" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh (waterLevel'=waterLevel{m ↦ MEDIUM})" org.eventb.core.prGoal="p49" org.eventb.core.prHyps="p50">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p51">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps=""/>
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p51" org.eventb.core.prHyps="p9,p5,p6,p7,p2,p10,p8,p4,p11,p34,p45,p17,p18,p19,p20,p21,p22,p23,p46,p30,p47,p48,p50">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p50"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prHyps="p27,p36">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p45"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (waterLevel(m)=MEDIUM)" org.eventb.core.prGoal="p49" org.eventb.core.prHyps="p27">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p52">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p47" org.eventb.core.prInfHyps="p40"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p46,p47,p48"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p52" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p53">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p40" org.eventb.core.prInfHyps="p42"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p40"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.falseHyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊥ hyp" org.eventb.core.prHyps="p42"/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p27"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="2" org.eventb.core.prHyps="p27,p35">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p45"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (waterLevel(m)=MEDIUM)" org.eventb.core.prGoal="p49" org.eventb.core.prHyps="p27">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p52">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p47" org.eventb.core.prInfHyps="p40"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p46,p47,p48"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p52" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p53">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p40" org.eventb.core.prInfHyps="p42"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p40"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.falseHyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊥ hyp" org.eventb.core.prHyps="p42"/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p27"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="3" org.eventb.core.prHyps="p13,p50">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p45"/>
<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.prGoal="p49" org.eventb.core.prHyps="p13">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p54">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p30" org.eventb.core.prInfHyps="p40"/>
<org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p20,p46,p30,p48"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p54" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p55">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p40" org.eventb.core.prInfHyps="p42"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p40"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.falseHyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊥ hyp" org.eventb.core.prHyps="p42"/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p13"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p46"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p34"/>
</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.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p34"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prIdent name="waterLevel'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p27" org.eventb.core.predicate="waterLevel(m)=MEDIUM"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p47" org.eventb.core.predicate="¬MEDIUM=waterLevel(m)"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ waterLevel(m)})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(waterLevel(m)=waterLevel(m)∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p40" org.eventb.core.predicate="¬waterLevel(m)=waterLevel(m)"/>
<org.eventb.core.prPred name="p54" org.eventb.core.predicate="waterLevel'∈MINE → {waterLevel(m),MEDIUM,waterLevel(m)}"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="¬MEDIUM=HIGH"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p24" org.eventb.core.predicate="LEVEL={waterLevel(m),MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p30" org.eventb.core.predicate="¬LOW=waterLevel(m)"/>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="MINE_SET={M}"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p35" org.eventb.core.predicate="waterLevel'=waterLevel{m ↦ waterLevel(m)}"/>
<org.eventb.core.prPred name="p26" org.eventb.core.predicate="¬waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p41" org.eventb.core.predicate="waterLevel'∈MINE → {waterLevel(m),waterLevel(m),HIGH}"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p25" org.eventb.core.predicate="¬waterLevel(m)=MEDIUM"/>
<org.eventb.core.prPred name="p45" org.eventb.core.predicate="waterLevel'=waterLevel{m ↦ MEDIUM}∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ waterLevel(m)})∨(waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p44" org.eventb.core.predicate="(waterLevel(m)=waterLevel(m)∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ waterLevel(m)})∨(waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="¬LOW=MEDIUM"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p51" org.eventb.core.predicate="waterLevel{m ↦ MEDIUM}∈MINE → {LOW,MEDIUM,waterLevel(m)}"/>
<org.eventb.core.prPred name="p34" org.eventb.core.predicate="waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p48" org.eventb.core.predicate="waterLevel∈MINE → {LOW,MEDIUM,waterLevel(m)}"/>
<org.eventb.core.prPred name="p49" org.eventb.core.predicate="waterLevel'∈MINE → {LOW,MEDIUM,waterLevel(m)}"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p50" org.eventb.core.predicate="waterLevel'=waterLevel{m ↦ MEDIUM}"/>
<org.eventb.core.prPred name="p42" org.eventb.core.predicate="⊥"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="¬LOW=HIGH"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p53" org.eventb.core.predicate="waterLevel'∈MINE → {LOW,waterLevel(m)}"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p43" org.eventb.core.predicate="waterLevel'∈MINE → {waterLevel(m),HIGH}"/>
<org.eventb.core.prPred name="p38" org.eventb.core.predicate="waterLevel'=waterLevel{m ↦ HIGH}"/>
<org.eventb.core.prPred name="p52" org.eventb.core.predicate="waterLevel'∈MINE → {LOW,waterLevel(m),waterLevel(m)}"/>
<org.eventb.core.prPred name="p28" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ waterLevel(m)})∨(waterLevel(m)=waterLevel(m)∧waterLevel'=waterLevel{m ↦ LOW})∨(waterLevel(m)=waterLevel(m)∧waterLevel'=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ waterLevel(m)})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="waterLevel(m)=LOW∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(waterLevel(m)=MEDIUM∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))"/>
<org.eventb.core.prPred name="p46" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,waterLevel(m)}"/>
<org.eventb.core.prPred name="p37" org.eventb.core.predicate="waterLevel{m ↦ LOW}∈MINE → {LOW,waterLevel(m),HIGH}"/>
<org.eventb.core.prPred name="p39" org.eventb.core.predicate="waterLevel{m ↦ HIGH}∈MINE → {LOW,waterLevel(m),HIGH}"/>
<org.eventb.core.prPred name="p32" org.eventb.core.predicate="waterLevel∈MINE → {LOW,waterLevel(m),HIGH}"/>
<org.eventb.core.prPred name="p31" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ waterLevel(m)})∨waterLevel'=waterLevel{m ↦ LOW}∨waterLevel'=waterLevel{m ↦ HIGH}∨(waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ waterLevel(m)})"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="waterLevel'∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ waterLevel(m)})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨waterLevel'=waterLevel{m ↦ MEDIUM}"/>
<org.eventb.core.prPred name="p33" org.eventb.core.predicate="waterLevel'∈MINE → {LOW,waterLevel(m),HIGH}"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel(m)=LOW"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p36" org.eventb.core.predicate="waterLevel'=waterLevel{m ↦ LOW}"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p29" org.eventb.core.predicate="LEVEL={LOW,waterLevel(m),HIGH}"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))))"/>
<org.eventb.core.prPred name="p55" org.eventb.core.predicate="waterLevel'∈MINE → {waterLevel(m),MEDIUM}"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="updateWaterLevel/act1/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="waterLevel0'" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3" org.eventb.core.prSets="LEVEL,MINE_SET" org.eventb.core.psManual="true">
<org.eventb.core.prRule name="org.eventb.core.seqprover.totalDom:2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="total function dom substitution in goal" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p3">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p4">
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p4" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p5">
<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="p6"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.conj" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p5" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p1" org.eventb.core.prHyps="p1"/>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p2">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p2" org.eventb.core.prHyps="p2"/>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="2" org.eventb.core.prGoal="p7">
<org.eventb.core.prRule name="org.eventb.core.seqprover.allI" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∀ goal (frees waterLevel0')" org.eventb.core.prGoal="p7" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p8">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.totalDom:2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="total function dom substitution in goal" org.eventb.core.prGoal="p8" org.eventb.core.prHyps="p3">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p9">
<org.eventb.core.prRule name="org.eventb.core.seqprover.totalDom:2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="total function dom substitution in goal" org.eventb.core.prGoal="p9" org.eventb.core.prHyps="p3">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p10">
<org.eventb.core.prRule name="org.eventb.core.seqprover.totalDom:2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="total function dom substitution in goal" org.eventb.core.prGoal="p10" org.eventb.core.prHyps="p3">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p11">
<org.eventb.core.prRule name="org.eventb.core.seqprover.disjToImplRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∨ to ⇒ in goal" org.eventb.core.prGoal="p11" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p12">
<org.eventb.core.prRule name="org.eventb.core.seqprover.impI" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p12" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p14" org.eventb.core.prHyps="p13">
<org.eventb.core.prRule name="org.eventb.core.seqprover.conj" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p14" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p1" org.eventb.core.prHyps="p1"/>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p2">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p2" org.eventb.core.prHyps="p2"/>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="2" org.eventb.core.prGoal="p15">
<org.eventb.core.prRule name="org.eventb.core.seqprover.impI" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p15" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p17" org.eventb.core.prHyps="p16">
<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="p1">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p1" org.eventb.core.prHyps="p1"/>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p2">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p2" org.eventb.core.prHyps="p2"/>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="2" org.eventb.core.prGoal="p18">
<org.eventb.core.prRule name="org.eventb.core.seqprover.impI" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p18" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p20" org.eventb.core.prHyps="p19">
<org.eventb.core.prRule name="org.eventb.core.seqprover.conj" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p20" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p1" org.eventb.core.prHyps="p1"/>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prGoal="p2">
<org.eventb.core.prRule name="org.eventb.core.seqprover.hyp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p2" org.eventb.core.prHyps="p2"/>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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="1.2.1.2.1.0.1"/>
<org.eventb.core.prExprRef name=".subst" org.eventb.core.prRef="e0"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue="1.2.1.0.1"/>
<org.eventb.core.prExprRef name=".subst" org.eventb.core.prRef="e0"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prString name=".pos" org.eventb.core.prSValue="1.0.1"/>
<org.eventb.core.prExprRef name=".subst" org.eventb.core.prRef="e0"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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="1.0.1"/>
<org.eventb.core.prExprRef name=".subst" org.eventb.core.prRef="e0"/>
</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="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="p20" org.eventb.core.predicate="m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="¬(waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ HIGH})">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="¬(waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ LOW})">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel0'=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))))">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="∀waterLevel'⦂ℙ(MINE_SET×LEVEL)·m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL))))))"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel0'=waterLevel{m ↦ MEDIUM})∨(m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ LOW})∨(m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))))">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel0'=waterLevel{m ↦ MEDIUM})∨(m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))))">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="∀waterLevel'⦂ℙ(MINE_SET×LEVEL)·(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))))"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="¬(waterLevel(m)=HIGH∧waterLevel0'=waterLevel{m ↦ MEDIUM})">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel0'=waterLevel{m ↦ MEDIUM})∨(m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ LOW})∨(m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ HIGH})∨(m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL)))))">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧(¬(waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ HIGH})⇒m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL)">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="¬(waterLevel(m)=HIGH∧waterLevel0'=waterLevel{m ↦ MEDIUM})⇒m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧(¬(waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ LOW})⇒m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧(¬(waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ HIGH})⇒m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL))">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="¬(waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ LOW})⇒m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧(¬(waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ HIGH})⇒m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL)">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="¬(waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ HIGH})⇒m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧(¬(waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ LOW})⇒m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧(¬(waterLevel(m)=MEDIUM∧waterLevel0'=waterLevel{m ↦ HIGH})⇒m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL))">
<org.eventb.core.prIdent name="waterLevel0'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="∀waterLevel'⦂ℙ(MINE_SET×LEVEL)·m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL))))))"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="m∈MINE∧waterLevel∈MINE_SET ⇸ LEVEL∧(∀waterLevel'⦂ℙ(MINE_SET×LEVEL)·(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL))))))"/>
<org.eventb.core.prExpr name="e0" org.eventb.core.expression="MINE"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="updateWaterLevel/act1/FIS" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10" org.eventb.core.prSets="LEVEL,MINE_SET,ONOFF" org.eventb.core.psManual="true">
<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="p10" org.eventb.core.prInfHyps="p11,p12"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p10"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p11,p12"/>
<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="p13,p14,p15,p16"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p13,p14,p15,p16"/>
<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="p17"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p17"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p18">
<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="p19"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.disjToImplRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∨ to ⇒ in goal" org.eventb.core.prGoal="p18" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p20">
<org.eventb.core.prRule name="org.eventb.core.seqprover.impI" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p20" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p22" org.eventb.core.prHyps="p21">
<org.eventb.core.prRule name="org.eventb.core.seqprover.disjToImplRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∨ to ⇒ in goal" org.eventb.core.prGoal="p22" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p23">
<org.eventb.core.prRule name="org.eventb.core.seqprover.impI" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p23" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p25" org.eventb.core.prHyps="p24">
<org.eventb.core.prRule name="org.eventb.core.seqprover.disjToImplRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∨ to ⇒ in goal" org.eventb.core.prGoal="p25" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p26">
<org.eventb.core.prRule name="org.eventb.core.seqprover.impI" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⇒ goal" org.eventb.core.prGoal="p26" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p28" org.eventb.core.prHyps="p27">
<org.eventb.core.prRule name="org.eventb.core.seqprover.disjE" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∨ hyp (waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH)" org.eventb.core.prHyps="p6">
<org.eventb.core.prAnte name="0" org.eventb.core.prHyps="p29">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p6"/>
<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.prGoal="p28" org.eventb.core.prHyps="p29">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p34">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p13" org.eventb.core.prInfHyps="p30"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p14" org.eventb.core.prInfHyps="p31"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p15" org.eventb.core.prInfHyps="p32"/>
<org.eventb.core.prHypAction name="FORWARD_INF3" org.eventb.core.prHyps="p24" org.eventb.core.prInfHyps="p33"/>
<org.eventb.core.prHypAction name="DESELECT4" org.eventb.core.prHyps="p13,p14,p15,p24"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p34" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p35">
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p35" org.eventb.core.prHyps="p9,p4,p5,p6,p2,p8,p7,p11,p12,p13,p14,p15,p16,p17,p21,p24,p27,p29,p30,p31,p32,p33">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p29"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="1" org.eventb.core.prHyps="p36">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p6"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.he" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="he (waterLevel(m)=MEDIUM)" org.eventb.core.prGoal="p28" org.eventb.core.prHyps="p36">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p42">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p13" org.eventb.core.prInfHyps="p37"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p14" org.eventb.core.prInfHyps="p38"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p16" org.eventb.core.prInfHyps="p32"/>
<org.eventb.core.prHypAction name="FORWARD_INF3" org.eventb.core.prHyps="p21" org.eventb.core.prInfHyps="p39"/>
<org.eventb.core.prHypAction name="FORWARD_INF4" org.eventb.core.prHyps="p24" org.eventb.core.prInfHyps="p40"/>
<org.eventb.core.prHypAction name="FORWARD_INF5" org.eventb.core.prHyps="p27" org.eventb.core.prInfHyps="p41"/>
<org.eventb.core.prHypAction name="DESELECT6" org.eventb.core.prHyps="p13,p14,p16,p21,p24,p27"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p40" org.eventb.core.prInfHyps="p43"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p40"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p41" org.eventb.core.prInfHyps="p44"/>
<org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p41"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.contr" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ct hyp (¬(∃waterLevel'·waterLevel'=waterLevel{m ↦ LOW}))" org.eventb.core.prGoal="p42" org.eventb.core.prHyps="p43">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p46" org.eventb.core.prHyps="p45">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p43"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.contr" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ct hyp (¬(∃waterLevel'·waterLevel'=waterLevel{m ↦ HIGH}))" org.eventb.core.prGoal="p46" org.eventb.core.prHyps="p44">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p47" org.eventb.core.prHyps="p43">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p44"/>
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p47" org.eventb.core.prHyps="p9,p4,p5,p6,p2,p8,p7,p11,p12,p13,p14,p15,p16,p17,p21,p24,p27,p36,p37,p38,p32,p39,p43,p44,p45">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p36"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prAnte name="2" org.eventb.core.prHyps="p48">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p6"/>
<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="p48">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p13" org.eventb.core.prInfHyps="p49"/>
<org.eventb.core.prHypAction name="FORWARD_INF1" org.eventb.core.prHyps="p15" org.eventb.core.prInfHyps="p38"/>
<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p16" org.eventb.core.prInfHyps="p50"/>
<org.eventb.core.prHypAction name="FORWARD_INF3" org.eventb.core.prHyps="p21" org.eventb.core.prInfHyps="p51"/>
<org.eventb.core.prHypAction name="FORWARD_INF4" org.eventb.core.prHyps="p27" org.eventb.core.prInfHyps="p33"/>
<org.eventb.core.prHypAction name="DESELECT5" org.eventb.core.prHyps="p13,p15,p16,p21,p27"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p51" org.eventb.core.prInfHyps="p52"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p51"/>
<org.eventb.core.prRule name="org.eventb.core.seqprover.contr" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ct hyp (¬(∃waterLevel'·waterLevel'=waterLevel{m ↦ MEDIUM}))" org.eventb.core.prGoal="p28" org.eventb.core.prHyps="p52">
<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p35" org.eventb.core.prHyps="p53">
<org.eventb.core.prHypAction name="DESELECT0" org.eventb.core.prHyps="p52"/>
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p35" org.eventb.core.prHyps="p9,p4,p5,p6,p2,p8,p7,p11,p12,p13,p14,p15,p16,p17,p21,p24,p27,p48,p49,p38,p50,p33,p52,p53">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
<org.eventb.core.prPredRef name=".pred" org.eventb.core.prRef="p48"/>
</org.eventb.core.prRule>
</org.eventb.core.prAnte>
</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.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.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.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="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="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p35" org.eventb.core.predicate="∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel'=waterLevel{m ↦ MEDIUM}"/>
<org.eventb.core.prPred name="p36" org.eventb.core.predicate="waterLevel(m)=MEDIUM"/>
<org.eventb.core.prPred name="p44" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel'=waterLevel{m ↦ HIGH})"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})⇒(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p50" org.eventb.core.predicate="¬MEDIUM=waterLevel(m)"/>
<org.eventb.core.prPred name="p51" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=waterLevel(m)∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p33" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ waterLevel(m)})"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="¬MEDIUM=HIGH"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p30" org.eventb.core.predicate="LEVEL={waterLevel(m),MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p38" org.eventb.core.predicate="¬LOW=waterLevel(m)"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="MINE_SET={M}"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p32" org.eventb.core.predicate="¬waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,HIGH}"/>
<org.eventb.core.prPred name="p31" org.eventb.core.predicate="¬waterLevel(m)=MEDIUM"/>
<org.eventb.core.prPred name="p24" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})"/>
<org.eventb.core.prPred name="p40" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=waterLevel(m)∧waterLevel'=waterLevel{m ↦ LOW})"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="¬LOW=MEDIUM"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})⇒(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p48" org.eventb.core.predicate="waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p45" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ waterLevel(m)})"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·(waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="¬LOW=HIGH"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p42" org.eventb.core.predicate="∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ waterLevel(m)}"/>
<org.eventb.core.prPred name="p34" org.eventb.core.predicate="∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=waterLevel(m)∧waterLevel'=waterLevel{m ↦ MEDIUM}"/>
<org.eventb.core.prPred name="p53" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="¬ON=OFF"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ MEDIUM})∨(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ LOW})∨(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="waterLevel(m)=LOW∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧(waterLevel(m)=MEDIUM∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))"/>
<org.eventb.core.prPred name="p47" org.eventb.core.predicate="∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel'=waterLevel{m ↦ HIGH}"/>
<org.eventb.core.prPred name="p39" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=HIGH∧waterLevel'=waterLevel{m ↦ waterLevel(m)})"/>
<org.eventb.core.prPred name="p49" org.eventb.core.predicate="LEVEL={LOW,MEDIUM,waterLevel(m)}"/>
<org.eventb.core.prPred name="p26" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})⇒(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p41" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=waterLevel(m)∧waterLevel'=waterLevel{m ↦ HIGH})"/>
<org.eventb.core.prPred name="p43" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel'=waterLevel{m ↦ LOW})"/>
<org.eventb.core.prPred name="p27" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})"/>
<org.eventb.core.prPred name="p28" org.eventb.core.predicate="∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM}"/>
<org.eventb.core.prPred name="p25" org.eventb.core.predicate="(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=MEDIUM∧waterLevel'=waterLevel{m ↦ HIGH})∨(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel(m)=LOW∧waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p29" org.eventb.core.predicate="waterLevel(m)=LOW"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p52" org.eventb.core.predicate="¬(∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel'=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="ONOFF={ON,OFF}"/>
<org.eventb.core.prPred name="p37" org.eventb.core.predicate="LEVEL={LOW,waterLevel(m),HIGH}"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p46" org.eventb.core.predicate="∃waterLevel'⦂ℙ(MINE_SET×LEVEL)·waterLevel'=waterLevel{m ↦ LOW}"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="addMine/MinePump_inv5/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7" org.eventb.core.prSets="LEVEL,MINE_SET,ONOFF">
<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p6,p2,p1,p4,p5,p3,p7">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="waterLevel{M ↦ LOW}∈{M} → LEVEL"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="MINE=(∅ ⦂ ℙ(MINE_SET))"/>
</org.eventb.core.prProof>
</org.eventb.core.prFile>
