<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.prFile version="1">
<org.eventb.core.prProof name="trigger_alarm/grd2/WD" 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,p13,p14,p15,p16" 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="p15,p9,p7,p12,p16,p10,p3,p13,p14,p8,p11,p4,p1,p2,p6,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<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="trigger_alarm/grd3/WD" 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,p13,p14,p15,p16,p17,p18,p19" 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="p18,p12,p10,p15,p19,p13,p4,p16,p17,p11,p14,p5,p1,p3,p7,p6,p2,p9,p8">
<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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="methane(m)=TRUE"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="methane∈MINE_SET ⇸ BOOL"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="m∈dom(methane)"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(bell)∧bell∈MINE_SET ⇸ BOOL"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="trigger_alarm/act1/SIM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22" 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="p21,p13,p11,p17,p22,p14,p4,p19,p20,p12,p15,p5,p1,p3,p7,p6,p2,p10,p9,p8,p18,p16">
<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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="methane(m)=TRUE"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="bell(m)=FALSE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="methane∈MINE_SET ⇸ BOOL"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="m∈dom(methane)"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="bell{m ↦ TRUE}=bell{m ↦ TRUE}"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="bell∈MINE_SET ⇸ BOOL"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="m∈dom(bell)"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="methane_leak/act1/SIM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16" 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="p15,p9,p7,p12,p16,p10,p3,p13,p14,p8,p11,p4,p1,p2,p6,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="methane{m ↦ TRUE}=methane{m ↦ TRUE}"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="high_water_detected/grd1/WD" 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,p13,p14,p15,p16" 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="p15,p9,p7,p12,p16,p10,p3,p13,p14,p8,p11,p4,p1,p2,p6,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="high_water_detected/grd3/WD" 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,p13,p14,p15,p16,p17,p18,p19" 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="p18,p12,p8,p15,p19,p13,p3,p16,p17,p9,p14,p4,p1,p2,p7,p5,p11,p10,p6">
<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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<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/grd4/WD" 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,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22" 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="p20,p14,p10,p17,p21,p15,p3,p18,p19,p11,p16,p4,p1,p2,p7,p5,p13,p12,p6,p22,p9,p8">
<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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="methane∈MINE_SET ⇸ BOOL"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="m∈dom(methane)"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p14" 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="p16" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="methane(m)=FALSE"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="high_water_detected/act1/SIM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22,p23,p24,p25,p26" 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="p12,p21,p18,p22,p11,p8,p14,p24,p23,p19,p9,p2,p13,p1,p4,p15,p20,p7,p3,p26,p5,p6,p16,p25,p17,p10">
<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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="methane∈MINE_SET ⇸ BOOL"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="m∈dom(methane)"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="(pump(m)=OFF∧pump{m ↦ ON}=pump{m ↦ ON})∨(m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF)"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="(pump(m)=OFF∧pump{m ↦ ON}=pump{m ↦ ON})∨(pump(m)=ON∧pump{m ↦ ON}=pump{m ↦ OFF})"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="pump(m)=OFF"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="pump∈MINE_SET ⇸ ONOFF"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p24" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p25" org.eventb.core.predicate="m∈dom(pump)"/>
<org.eventb.core.prPred name="p26" org.eventb.core.predicate="methane(m)=FALSE"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="low_water_detected/grd2/WD" 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,p13,p14,p15,p16" 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="p15,p9,p7,p12,p16,p10,p3,p13,p14,p8,p11,p4,p1,p2,p6,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="low_water_detected/grd3/WD" 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,p13,p14,p15,p16,p17,p18,p19" 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="p18,p12,p9,p15,p19,p13,p3,p16,p17,p10,p14,p4,p1,p2,p7,p5,p8,p11,p6">
<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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="waterLevel(m)=LOW"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="low_water_detected/act1/SIM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22,p23" 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="p22,p14,p11,p17,p23,p15,p3,p19,p20,p12,p16,p4,p1,p2,p8,p5,p10,p13,p6,p18,p21,p9,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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="(pump(m)=OFF∧pump{m ↦ OFF}=pump{m ↦ ON})∨(m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF)"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="pump∈MINE_SET ⇸ ONOFF"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="waterLevel(m)=LOW"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p14" 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="p16" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="pump(m)=ON"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="(pump(m)=OFF∧pump{m ↦ OFF}=pump{m ↦ ON})∨(pump(m)=ON∧pump{m ↦ OFF}=pump{m ↦ OFF})"/>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="m∈dom(pump)"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="methane_detected/grd3/WD" 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,p13,p14,p15,p16" 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="p15,p9,p7,p12,p16,p10,p3,p13,p14,p8,p11,p4,p1,p2,p6,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="methane_detected/grd4/WD" 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,p13,p14,p15,p16,p17,p18,p19" 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="p18,p10,p8,p13,p19,p11,p3,p15,p16,p9,p12,p4,p1,p2,p6,p5,p14,p17,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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="pump∈MINE_SET ⇸ ONOFF"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p14" 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="p18" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="m∈dom(pump)"/>
<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="methane_detected/act1/SIM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22,p23" 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="p22,p14,p12,p17,p23,p15,p4,p19,p20,p13,p16,p5,p1,p3,p8,p6,p18,p21,p9,p2,p11,p10,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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="methane(m)=TRUE"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="(pump(m)=OFF∧pump{m ↦ OFF}=pump{m ↦ ON})∨(m∈dom(pump)∧pump∈MINE_SET ⇸ ONOFF)"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="pump∈MINE_SET ⇸ ONOFF"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="methane∈MINE_SET ⇸ BOOL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="m∈dom(methane)"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p14" 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="p16" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="pump(m)=ON"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="(pump(m)=OFF∧pump{m ↦ OFF}=pump{m ↦ ON})∨(pump(m)=ON∧pump{m ↦ OFF}=pump{m ↦ OFF})"/>
<org.eventb.core.prPred name="p23" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p22" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
<org.eventb.core.prPred name="p21" org.eventb.core.predicate="m∈dom(pump)"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="high_to_medium/grd2/WD" 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,p13,p14,p15,p16" 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="p15,p9,p7,p12,p16,p10,p3,p13,p14,p8,p11,p4,p1,p2,p6,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="high_to_medium/act1/SIM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20" 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="p19,p12,p8,p15,p20,p13,p3,p16,p17,p9,p14,p4,p1,p2,p7,p5,p11,p10,p6,p18">
<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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))))"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="medium_to_low/grd2/WD" 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,p13,p14,p15,p16" 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="p15,p9,p7,p12,p16,p10,p3,p13,p14,p8,p11,p4,p1,p2,p6,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="medium_to_low/act1/SIM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20" 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="p19,p13,p10,p16,p20,p14,p4,p17,p18,p11,p15,p5,p1,p3,p9,p6,p2,p12,p8,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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ LOW}=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ LOW}=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ LOW}=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel{m ↦ LOW}=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="waterLevel(m)=MEDIUM"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ LOW}=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel{m ↦ LOW}=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel{m ↦ LOW}=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))))"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="low_to_medium/grd2/WD" 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,p13,p14,p15,p16" 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="p15,p9,p7,p12,p16,p10,p3,p13,p14,p8,p11,p4,p1,p2,p6,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="low_to_medium/act1/SIM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20" 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="p19,p12,p9,p15,p20,p13,p3,p16,p17,p10,p14,p4,p1,p2,p7,p5,p8,p11,p6,p18">
<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="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="waterLevel(m)=LOW"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))))"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="medium_to_high/grd2/WD" 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,p13,p14,p15,p16" 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="p15,p9,p7,p12,p16,p10,p3,p13,p14,p8,p11,p4,p1,p2,p6,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.prIdent name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.prIdent name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.prIdent name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.prIdent name="bell" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<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="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="p1" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="MINE⊆MINE_SET"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<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="p6" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="medium_to_high/act1/SIM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20" 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="p19,p13,p10,p16,p20,p14,p5,p17,p18,p11,p15,p6,p2,p4,p9,p7,p3,p12,p8,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="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="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="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="p1" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ MEDIUM})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ LOW})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL∧((waterLevel(m)=MEDIUM∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ HIGH})∨(m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL)))))"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF"/>
<org.eventb.core.prPred name="p3" 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="p0" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ MEDIUM})"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="methane∈MINE → BOOL"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="dom(waterLevel)=MINE"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="m∈MINE"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="waterLevel∈MINE_SET ⇸ LEVEL"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="partition(MINE_SET,{M})"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(bell)=MINE"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="m∈dom(waterLevel)"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})"/>
<org.eventb.core.prPred name="p14" org.eventb.core.predicate="bell∈MINE → BOOL"/>
<org.eventb.core.prPred name="p15" org.eventb.core.predicate="dom(methane)=MINE"/>
<org.eventb.core.prPred name="p16" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)"/>
<org.eventb.core.prPred name="p18" org.eventb.core.predicate="dom(pump)=MINE"/>
<org.eventb.core.prPred name="p17" org.eventb.core.predicate="waterLevel∈MINE → LEVEL"/>
<org.eventb.core.prPred name="p20" org.eventb.core.predicate="pump∈MINE → ONOFF"/>
<org.eventb.core.prPred name="p19" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})"/>
</org.eventb.core.prProof>
</org.eventb.core.prFile>
