<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.prFile version="1">
<org.eventb.core.prProof name="INITIALISATION/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1" org.eventb.core.prSets="TRAIN_MODE">
<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">
<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.prPred name="p1" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="(∅ ⦂ ℙ(TRAIN_SET×BOOL))∈(∅ ⦂ ℙ(TRAIN_SET)) → BOOL"/>
</org.eventb.core.prProof>
<org.eventb.core.prProof name="updateOnCBTC/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5" org.eventb.core.prSets="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,p5,p3,p4,p2">
<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="onCBTC" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.prIdent name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.prIdent name="v" org.eventb.core.type="BOOL"/>
<org.eventb.core.prPred name="p0" org.eventb.core.predicate="onCBTC{t ↦ v}∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})"/>
<org.eventb.core.prPred name="p3" org.eventb.core.predicate="onCBTC∈TRAIN → BOOL"/>
<org.eventb.core.prPred name="p2" org.eventb.core.predicate="v∈BOOL"/>
<org.eventb.core.prPred name="p4" org.eventb.core.predicate="t∈TRAIN"/>
<org.eventb.core.prPred name="p5" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)"/>
</org.eventb.core.prProof>
</org.eventb.core.prFile>
