<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.prFile version="1">
<org.eventb.core.prProof name="updateOnCBTC/onCBTC/EQL" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p0" org.eventb.core.prInfHyps="p1,p2,p3,p4"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p0"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p1,p2,p3,p4"/>
<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="p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
</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.prPred name="p1" org.eventb.core.predicate="TRAIN_MODE={ATP,ATPR,BYPASS}">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN_MODE" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN_MODE" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="¬ATPR=BYPASS">
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="v∈BOOL">
<org.eventb.core.prIdent name="v" org.eventb.core.type="BOOL"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬ATP=BYPASS">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)">
<org.eventb.core.prIdent name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.prIdent name="TRAIN_SET" org.eventb.core.type="ℙ(TRAIN_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬ATP=ATPR">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="updateDesiredTrainMode/desiredTrainMode/EQL" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p0" org.eventb.core.prInfHyps="p1,p2,p3,p4"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p0"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p1,p2,p3,p4"/>
<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="p5"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
</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.prPred name="p1" org.eventb.core.predicate="TRAIN_MODE={ATP,ATPR,BYPASS}">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN_MODE" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN_MODE" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="¬ATPR=BYPASS">
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬ATP=BYPASS">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="mode∈TRAIN_MODE">
<org.eventb.core.prIdent name="TRAIN_MODE" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
<org.eventb.core.prIdent name="mode" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)">
<org.eventb.core.prIdent name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.prIdent name="TRAIN_SET" org.eventb.core.type="ℙ(TRAIN_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬ATP=ATPR">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="ATPRModeSelected/grd1/GRD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p0" org.eventb.core.prInfHyps="p1,p2,p3,p4"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p0"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p1,p2,p3,p4"/>
<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="p5"/>
</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.prPred name="p1" org.eventb.core.predicate="TRAIN_MODE={ATP,ATPR,BYPASS}">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN_MODE" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN_MODE" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="¬ATPR=BYPASS">
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬ATP=BYPASS">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)">
<org.eventb.core.prIdent name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.prIdent name="TRAIN_SET" org.eventb.core.type="ℙ(TRAIN_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬ATP=ATPR">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="ATPRModeSelected/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" org.eventb.core.prSets="TRAIN_MODE,TRAIN_SET">
<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,p8,p4,p2,p7,p3,p5,p9,p10,p6">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.prIdent name="desiredTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.prIdent name="effectiveTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.prIdent name="emergencyBrake" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="onCBTC" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="effectiveTrainMode∈TRAIN → TRAIN_MODE"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="desiredTrainMode∈TRAIN → TRAIN_MODE"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="onCBTC∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="effectiveTrainMode{t ↦ ATPR}=effectiveTrainMode{t ↦ ATPR}"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="t∈TRAIN"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="desiredTrainMode∈TRAIN_SET ⇸ TRAIN_MODE"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="emergencyBrake∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="desiredTrainMode(t)=ATPR"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="t∈dom(desiredTrainMode)"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="ATPRModeSelected/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" org.eventb.core.prSets="TRAIN_MODE,TRAIN_SET">
<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,p7,p4,p2,p6,p3,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.prIdent name="desiredTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.prIdent name="effectiveTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.prIdent name="emergencyBrake" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="onCBTC" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="effectiveTrainMode∈TRAIN → TRAIN_MODE"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="desiredTrainMode∈TRAIN → TRAIN_MODE"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="onCBTC∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="t∈TRAIN"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="emergencyBrake∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="t∈dom(desiredTrainMode)∧desiredTrainMode∈TRAIN_SET ⇸ TRAIN_MODE"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="ATPModeSelectedOnCBTCTrack/grd1/GRD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
<org.eventb.core.prRule name="org.eventb.core.seqprover.partitionRewrites" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS}))" org.eventb.core.prHyps="">
<org.eventb.core.prAnte name="0">
<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p0" org.eventb.core.prInfHyps="p1,p2,p3,p4"/>
<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p0"/>
<org.eventb.core.prHypAction name="SELECT2" org.eventb.core.prHyps="p1,p2,p3,p4"/>
<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="p5"/>
</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.prPred name="p1" org.eventb.core.predicate="TRAIN_MODE={ATP,ATPR,BYPASS}">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN_MODE" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN_MODE" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="¬ATPR=BYPASS">
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬ATP=BYPASS">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)">
<org.eventb.core.prIdent name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.prIdent name="TRAIN_SET" org.eventb.core.type="ℙ(TRAIN_SET)"/>
</org.eventb.core.prPred>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬ATP=ATPR">
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.prPred>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="ATPModeSelectedOnCBTCTrack/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" org.eventb.core.prSets="TRAIN_MODE,TRAIN_SET">
<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,p10,p8,p6,p11,p7,p2,p9,p12,p13,p1,p4,p3">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.prIdent name="desiredTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.prIdent name="effectiveTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.prIdent name="emergencyBrake" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="onCBTC" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="desiredTrainMode(t)=ATP"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="t∈TRAIN"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="desiredTrainMode∈TRAIN_SET ⇸ TRAIN_MODE"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="t∈dom(desiredTrainMode)"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="effectiveTrainMode∈TRAIN → TRAIN_MODE"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="desiredTrainMode∈TRAIN → TRAIN_MODE"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="onCBTC∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="onCBTC(t)=TRUE"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)"/>
<org.eventb.core.prPred name="p11" org.eventb.core.predicate="emergencyBrake∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="effectiveTrainMode{t ↦ ATP}=effectiveTrainMode{t ↦ ATP}"/>
<org.eventb.core.prPred name="p13" org.eventb.core.predicate="onCBTC∈TRAIN_SET ⇸ BOOL"/>
<org.eventb.core.prPred name="p12" org.eventb.core.predicate="t∈dom(onCBTC)"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="ATPModeSelectedOnCBTCTrack/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" org.eventb.core.prSets="TRAIN_MODE,TRAIN_SET">
<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,p7,p4,p2,p6,p3,p5">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.prIdent name="desiredTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.prIdent name="effectiveTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.prIdent name="emergencyBrake" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="onCBTC" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="effectiveTrainMode∈TRAIN → TRAIN_MODE"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="desiredTrainMode∈TRAIN → TRAIN_MODE"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="onCBTC∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="t∈TRAIN"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="emergencyBrake∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="t∈dom(onCBTC)∧onCBTC∈TRAIN_SET ⇸ BOOL"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="ATPModeSelectedOnCBTCTrack/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" org.eventb.core.prSets="TRAIN_MODE,TRAIN_SET">
<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,p8,p4,p2,p7,p3,p6,p5,p10,p9">
<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
</org.eventb.core.prRule>
<org.eventb.core.prIdent name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.prIdent name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.prIdent name="desiredTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.prIdent name="effectiveTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.prIdent name="emergencyBrake" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="onCBTC" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="effectiveTrainMode∈TRAIN → TRAIN_MODE"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="desiredTrainMode∈TRAIN → TRAIN_MODE"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="onCBTC∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="onCBTC(t)=TRUE"/>
<org.eventb.core.prPred name="p6" org.eventb.core.predicate="t∈TRAIN"/>
<org.eventb.core.prPred name="p8" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)"/>
<org.eventb.core.prPred name="p7" org.eventb.core.predicate="emergencyBrake∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="t∈dom(desiredTrainMode)∧desiredTrainMode∈TRAIN_SET ⇸ TRAIN_MODE"/>
<org.eventb.core.prPred name="p10" org.eventb.core.predicate="t∈dom(onCBTC)"/>
<org.eventb.core.prPred name="p9" org.eventb.core.predicate="onCBTC∈TRAIN_SET ⇸ BOOL"/>
</org.eventb.core.prProof>
</org.eventb.core.prFile>
