Add hemodialysis machine (ABZ 2016 case study)

HD/.project

+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>HDMachine</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>org.rodinp.core.rodinbuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>org.rodinp.core.rodinnature</nature>
+	</natures>
+</projectDescription>

HD/c12-PM_limit.bpr

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.prFile version="1"/>
\ No newline at end of file

HD/c5-signals.bcc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
+<org.eventb.core.scAxiom name="'" org.eventb.core.label="SIGNAL_STATUS−def" org.eventb.core.predicate="partition(SIGNAL_STATUS,{SIGNAL_OFF},{SIGNAL_RED},{SIGNAL_GREEN},{SIGNAL_ORANGE})" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.axiom#+" org.eventb.core.theorem="false"/>
+<org.eventb.core.scCarrierSet name="SIGNAL" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.carrierSet#," org.eventb.core.type="ℙ(SIGNAL)"/>
+<org.eventb.core.scConstant name="SIGNAL_GREEN" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.constant#*" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.scConstant name="SIGNAL_OFF" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.constant#(" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.scConstant name="SIGNAL_ORANGE" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.constant#\/" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.scConstant name="SIGNAL_RED" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.constant#)" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.scCarrierSet name="SIGNAL_STATUS" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.carrierSet#'" org.eventb.core.type="ℙ(SIGNAL_STATUS)"/>
+</org.eventb.core.scContextFile>

HD/c5-signals.bpo

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.poFile org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
+<org.eventb.core.poIdentifier name="SIGNAL" org.eventb.core.type="ℙ(SIGNAL)"/>
+<org.eventb.core.poIdentifier name="SIGNAL_STATUS" org.eventb.core.type="ℙ(SIGNAL_STATUS)"/>
+<org.eventb.core.poIdentifier name="SIGNAL_GREEN" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.poIdentifier name="SIGNAL_OFF" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.poIdentifier name="SIGNAL_ORANGE" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.poIdentifier name="SIGNAL_RED" org.eventb.core.type="SIGNAL_STATUS"/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/HDMachine/c5-signals.bpo|org.eventb.core.poFile#c5-signals|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="partition(SIGNAL_STATUS,{SIGNAL_OFF},{SIGNAL_RED},{SIGNAL_GREEN},{SIGNAL_ORANGE})" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.axiom#+"/>
+</org.eventb.core.poPredicateSet>
+</org.eventb.core.poFile>

HD/c5-signals.bpr

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.prFile version="1"/>
\ No newline at end of file

HD/c5-signals.bps

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.psFile/>
\ No newline at end of file

HD/c5-signals.buc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd" version="3">
+<org.eventb.core.carrierSet name="'" org.eventb.core.identifier="SIGNAL_STATUS"/>
+<org.eventb.core.constant name="(" org.eventb.core.identifier="SIGNAL_OFF"/>
+<org.eventb.core.constant name=")" org.eventb.core.identifier="SIGNAL_RED"/>
+<org.eventb.core.constant name="*" org.eventb.core.identifier="SIGNAL_GREEN"/>
+<org.eventb.core.axiom name="+" org.eventb.core.label="SIGNAL_STATUS−def" org.eventb.core.predicate="partition(SIGNAL_STATUS, {SIGNAL_OFF}, {SIGNAL_RED}, {SIGNAL_GREEN}, {SIGNAL_ORANGE})"/>
+<org.eventb.core.carrierSet name="," org.eventb.core.identifier="SIGNAL"/>
+<org.eventb.core.constant name="/" org.eventb.core.identifier="SIGNAL_ORANGE"/>
+</org.eventb.core.contextFile>

HD/c6-CFTestingSignal.bcc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
+<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/HDMachine/c5-signals.bcc|org.eventb.core.scContextFile#c5-signals" org.eventb.core.source="/HDMachine/c6-CFTestingSignal.buc|org.eventb.core.contextFile#c6-CFTestingSignal|org.eventb.core.extendsContext#'"/>
+<org.eventb.core.scInternalContext name="c5-signals">
+<org.eventb.core.scAxiom name="'" org.eventb.core.label="SIGNAL_STATUS−def" org.eventb.core.predicate="partition(SIGNAL_STATUS,{SIGNAL_OFF},{SIGNAL_RED},{SIGNAL_GREEN},{SIGNAL_ORANGE})" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.axiom#+" org.eventb.core.theorem="false"/>
+<org.eventb.core.scCarrierSet name="SIGNAL" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.carrierSet#," org.eventb.core.type="ℙ(SIGNAL)"/>
+<org.eventb.core.scConstant name="SIGNAL_GREEN" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.constant#*" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.scConstant name="SIGNAL_OFF" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.constant#(" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.scConstant name="SIGNAL_ORANGE" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.constant#\/" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.scConstant name="SIGNAL_RED" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.constant#)" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.scCarrierSet name="SIGNAL_STATUS" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.carrierSet#'" org.eventb.core.type="ℙ(SIGNAL_STATUS)"/>
+</org.eventb.core.scInternalContext>
+<org.eventb.core.scAxiom name="c5-signalt" org.eventb.core.label="CF_TESTING_SIGNAL-type" org.eventb.core.predicate="CF_TESTING_SIGNAL∈SIGNAL" org.eventb.core.source="/HDMachine/c6-CFTestingSignal.buc|org.eventb.core.contextFile#c6-CFTestingSignal|org.eventb.core.axiom#)" org.eventb.core.theorem="true"/>
+<org.eventb.core.scConstant name="CF_TESTING_SIGNAL" org.eventb.core.source="/HDMachine/c6-CFTestingSignal.buc|org.eventb.core.contextFile#c6-CFTestingSignal|org.eventb.core.constant#(" org.eventb.core.type="SIGNAL"/>
+</org.eventb.core.scContextFile>

HD/c6-CFTestingSignal.bpo

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.poFile org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
+<org.eventb.core.poIdentifier name="SIGNAL" org.eventb.core.type="ℙ(SIGNAL)"/>
+<org.eventb.core.poIdentifier name="SIGNAL_STATUS" org.eventb.core.type="ℙ(SIGNAL_STATUS)"/>
+<org.eventb.core.poIdentifier name="SIGNAL_GREEN" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.poIdentifier name="SIGNAL_OFF" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.poIdentifier name="SIGNAL_ORANGE" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.poIdentifier name="SIGNAL_RED" org.eventb.core.type="SIGNAL_STATUS"/>
+<org.eventb.core.poPredicate name="SIGNAL_STATUT" org.eventb.core.predicate="partition(SIGNAL_STATUS,{SIGNAL_OFF},{SIGNAL_RED},{SIGNAL_GREEN},{SIGNAL_ORANGE})" org.eventb.core.source="/HDMachine/c5-signals.buc|org.eventb.core.contextFile#c5-signals|org.eventb.core.axiom#+"/>
+<org.eventb.core.poIdentifier name="CF_TESTING_SIGNAL" org.eventb.core.type="SIGNAL"/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/HDMachine/c6-CFTestingSignal.bpo|org.eventb.core.poFile#c6-CFTestingSignal|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="CF_TESTING_SIGNAL∈SIGNAL" org.eventb.core.source="/HDMachine/c6-CFTestingSignal.buc|org.eventb.core.contextFile#c6-CFTestingSignal|org.eventb.core.axiom#)"/>
+</org.eventb.core.poPredicateSet>
+</org.eventb.core.poFile>

HD/c6-CFTestingSignal.bpr

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.prFile version="1"/>
\ No newline at end of file

HD/c6-CFTestingSignal.bps

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.psFile/>
\ No newline at end of file

HD/c6-CFTestingSignal.buc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd" version="3">
+<org.eventb.core.extendsContext name="'" org.eventb.core.target="c5-signals"/>
+<org.eventb.core.constant name="(" org.eventb.core.identifier="CF_TESTING_SIGNAL"/>
+<org.eventb.core.axiom name=")" org.eventb.core.label="CF_TESTING_SIGNAL-type" org.eventb.core.predicate="CF_TESTING_SIGNAL ∈ SIGNAL" org.eventb.core.theorem="true"/>
+</org.eventb.core.contextFile>

HD/c7-concentrates.bcc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
+<org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1" org.eventb.core.predicate="partition(CONCENTRATE,{CONCENTRATE_NONE},{CONCENTRATE_BICARBONATE},{CONCENTRATE_ACETATE})" org.eventb.core.source="/HDMachine/c7-concentrates.buc|org.eventb.core.contextFile#c7-concentrates|org.eventb.core.axiom#+" org.eventb.core.theorem="false"/>
+<org.eventb.core.scCarrierSet name="CONCENTRATE" org.eventb.core.source="/HDMachine/c7-concentrates.buc|org.eventb.core.contextFile#c7-concentrates|org.eventb.core.carrierSet#'" org.eventb.core.type="ℙ(CONCENTRATE)"/>
+<org.eventb.core.scConstant name="CONCENTRATE_ACETATE" org.eventb.core.source="/HDMachine/c7-concentrates.buc|org.eventb.core.contextFile#c7-concentrates|org.eventb.core.constant#*" org.eventb.core.type="CONCENTRATE"/>
+<org.eventb.core.scConstant name="CONCENTRATE_BICARBONATE" org.eventb.core.source="/HDMachine/c7-concentrates.buc|org.eventb.core.contextFile#c7-concentrates|org.eventb.core.constant#)" org.eventb.core.type="CONCENTRATE"/>
+<org.eventb.core.scConstant name="CONCENTRATE_NONE" org.eventb.core.source="/HDMachine/c7-concentrates.buc|org.eventb.core.contextFile#c7-concentrates|org.eventb.core.constant#(" org.eventb.core.type="CONCENTRATE"/>
+</org.eventb.core.scContextFile>

HD/c7-concentrates.bpo

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.poFile org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
+<org.eventb.core.poIdentifier name="CONCENTRATE" org.eventb.core.type="ℙ(CONCENTRATE)"/>
+<org.eventb.core.poIdentifier name="CONCENTRATE_ACETATE" org.eventb.core.type="CONCENTRATE"/>
+<org.eventb.core.poIdentifier name="CONCENTRATE_BICARBONATE" org.eventb.core.type="CONCENTRATE"/>
+<org.eventb.core.poIdentifier name="CONCENTRATE_NONE" org.eventb.core.type="CONCENTRATE"/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/HDMachine/c7-concentrates.bpo|org.eventb.core.poFile#c7-concentrates|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="partition(CONCENTRATE,{CONCENTRATE_NONE},{CONCENTRATE_BICARBONATE},{CONCENTRATE_ACETATE})" org.eventb.core.source="/HDMachine/c7-concentrates.buc|org.eventb.core.contextFile#c7-concentrates|org.eventb.core.axiom#+"/>
+</org.eventb.core.poPredicateSet>
+</org.eventb.core.poFile>

HD/c7-concentrates.bpr

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.prFile version="1"/>
\ No newline at end of file

HD/c7-concentrates.bps

+<?xml version="1.0" encoding="UTF-8"?>
+<org.eventb.core.psFile/>
\ No newline at end of file

HD/c7-concentrates.buc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd" version="3">
+<org.eventb.core.carrierSet name="'" org.eventb.core.identifier="CONCENTRATE"/>
+<org.eventb.core.constant name="(" org.eventb.core.identifier="CONCENTRATE_NONE"/>
+<org.eventb.core.constant name=")" org.eventb.core.identifier="CONCENTRATE_BICARBONATE"/>
+<org.eventb.core.constant name="*" org.eventb.core.identifier="CONCENTRATE_ACETATE"/>
+<org.eventb.core.axiom name="+" org.eventb.core.label="axm1" org.eventb.core.predicate="partition(CONCENTRATE, {CONCENTRATE_NONE}, {CONCENTRATE_BICARBONATE}, {CONCENTRATE_ACETATE})"/>
+</org.eventb.core.contextFile>

HD/c8-rinsing_parameters.bcc

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase;de.prob.units.mchBase;org.animb.valuation.valBase">
+<org.eventb.core.scAxiom name="'" org.eventb.core.label="FILLING_BP_RATE_RANGE_type" org.eventb.core.predicate="FILLING_BP_RATE_RANGE=50 ‥ 600" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#(" org.eventb.core.theorem="false"/>
+<org.eventb.core.scAxiom name="(" org.eventb.core.label="FILLING_BP_RATE_RANGE_non_empty" org.eventb.core.predicate="FILLING_BP_RATE_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#7" org.eventb.core.theorem="true"/>
+<org.eventb.core.scAxiom name=")" org.eventb.core.label="FILL_BP_VOLUME_RANGE_type" org.eventb.core.predicate="FILLING_BP_VOLUME_RANGE=0 ‥ 6000" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#*" org.eventb.core.theorem="false"/>
+<org.eventb.core.scAxiom name="*" org.eventb.core.label="FILL_BP_VOLUME_RANGE_non_empty" org.eventb.core.predicate="FILLING_BP_VOLUME_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm1" org.eventb.core.theorem="true"/>
+<org.eventb.core.scAxiom name="+" org.eventb.core.label="RINSING_BP_RATE_RANGE_type" org.eventb.core.predicate="RINSING_BP_RATE_RANGE=50 ‥ 300" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#," org.eventb.core.theorem="false"/>
+<org.eventb.core.scAxiom name="," org.eventb.core.label="RINSING_BP_RATE_RANGE_non_empty" org.eventb.core.predicate="RINSING_BP_RATE_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm2" org.eventb.core.theorem="true"/>
+<org.eventb.core.scAxiom name="-" org.eventb.core.label="DF_FLOW_RANGE_type" org.eventb.core.predicate="DF_FLOW_RANGE=50 ‥ 300" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#." org.eventb.core.theorem="false"/>
+<org.eventb.core.scAxiom name="." org.eventb.core.label="DF_FLOW_RANGE_non_empty" org.eventb.core.predicate="DF_FLOW_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm3" org.eventb.core.theorem="true"/>
+<org.eventb.core.scAxiom name="/" org.eventb.core.label="RINSING_TIME_RANGE_type" org.eventb.core.predicate="RINSING_TIME_RANGE=0 ‥ 59" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#0" org.eventb.core.theorem="false"/>
+<org.eventb.core.scAxiom name="0" org.eventb.core.label="RINSING_TIME_RANGE_non_empty" org.eventb.core.predicate="RINSING_TIME_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm4" org.eventb.core.theorem="true"/>
+<org.eventb.core.scAxiom name="1" org.eventb.core.label="UF_RINSING_RATE_RANGE_type" org.eventb.core.predicate="UF_RINSING_RATE_RANGE=0 ‥ 3000" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#2" org.eventb.core.theorem="false"/>
+<org.eventb.core.scAxiom name="2" org.eventb.core.label="UF_RINSING_RATE_RANGE_non_empty" org.eventb.core.predicate="UF_RINSING_RATE_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm5" org.eventb.core.theorem="true"/>
+<org.eventb.core.scAxiom name="3" org.eventb.core.label="UF_RINSING_VOLUME_RANGE_type" org.eventb.core.predicate="UF_RINSING_VOLUME_RANGE=0 ‥ 2950" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#4" org.eventb.core.theorem="false"/>
+<org.eventb.core.scAxiom name="4" org.eventb.core.label="UF_RINSING_VOLUME_RANGE_non_empty" org.eventb.core.predicate="UF_RINSING_VOLUME_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm6" org.eventb.core.theorem="true"/>
+<org.eventb.core.scAxiom name="5" org.eventb.core.label="BLOOD_FLOW_RANGE_type" org.eventb.core.predicate="BLOOD_FLOW_RANGE=50 ‥ 600" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#6" org.eventb.core.theorem="false"/>
+<org.eventb.core.scAxiom name="6" org.eventb.core.label="BLOOD_FLOW_RANGE_non_empty" org.eventb.core.predicate="BLOOD_FLOW_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm7" org.eventb.core.theorem="true"/>
+<org.eventb.core.scConstant name="BLOOD_FLOW_RANGE" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.constant#5" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.scConstant name="DF_FLOW_RANGE" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.constant#-" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.scConstant name="FILLING_BP_RATE_RANGE" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.constant#'" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.scConstant name="FILLING_BP_VOLUME_RANGE" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.constant#)" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.scConstant name="RINSING_BP_RATE_RANGE" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.constant#+" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.scConstant name="RINSING_TIME_RANGE" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.constant#\/" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.scConstant name="UF_RINSING_RATE_RANGE" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.constant#1" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.scConstant name="UF_RINSING_VOLUME_RANGE" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.constant#3" org.eventb.core.type="ℙ(ℤ)"/>
+</org.eventb.core.scContextFile>

HD/c8-rinsing_parameters.bpo

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.poFile org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
+<org.eventb.core.poIdentifier name="BLOOD_FLOW_RANGE" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.poIdentifier name="DF_FLOW_RANGE" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.poIdentifier name="FILLING_BP_RATE_RANGE" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.poIdentifier name="FILLING_BP_VOLUME_RANGE" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.poIdentifier name="RINSING_BP_RATE_RANGE" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.poIdentifier name="RINSING_TIME_RANGE" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.poIdentifier name="UF_RINSING_RATE_RANGE" org.eventb.core.type="ℙ(ℤ)"/>
+<org.eventb.core.poIdentifier name="UF_RINSING_VOLUME_RANGE" org.eventb.core.type="ℙ(ℤ)"/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poSequent name="FILLING_BP_RATE_RANGE_non_empty/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP'"/>
+<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="FILLING_BP_RATE_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#7"/>
+<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#7"/>
+<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP'"/>
+</org.eventb.core.poSequent>
+<org.eventb.core.poSequent name="FILL_BP_VOLUME_RANGE_non_empty/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP)"/>
+<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="FILLING_BP_VOLUME_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm1"/>
+<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm1"/>
+<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP)"/>
+</org.eventb.core.poSequent>
+<org.eventb.core.poSequent name="RINSING_BP_RATE_RANGE_non_empty/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP+"/>
+<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="RINSING_BP_RATE_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm2"/>
+<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm2"/>
+<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP+"/>
+</org.eventb.core.poSequent>
+<org.eventb.core.poSequent name="DF_FLOW_RANGE_non_empty/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP-"/>
+<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="DF_FLOW_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm3"/>
+<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm3"/>
+<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP-"/>
+</org.eventb.core.poSequent>
+<org.eventb.core.poSequent name="RINSING_TIME_RANGE_non_empty/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP\/"/>
+<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="RINSING_TIME_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm4"/>
+<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm4"/>
+<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP\/"/>
+</org.eventb.core.poSequent>
+<org.eventb.core.poSequent name="UF_RINSING_RATE_RANGE_non_empty/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP1"/>
+<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="UF_RINSING_RATE_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm5"/>
+<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm5"/>
+<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP1"/>
+</org.eventb.core.poSequent>
+<org.eventb.core.poSequent name="UF_RINSING_VOLUME_RANGE_non_empty/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP3"/>
+<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="UF_RINSING_VOLUME_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm6"/>
+<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm6"/>
+<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP3"/>
+</org.eventb.core.poSequent>
+<org.eventb.core.poSequent name="BLOOD_FLOW_RANGE_non_empty/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP5"/>
+<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="BLOOD_FLOW_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm7"/>
+<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm7"/>
+<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP5"/>
+</org.eventb.core.poSequent>
+<org.eventb.core.poPredicateSet name="HYP'" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="FILLING_BP_RATE_RANGE=50 ‥ 600" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#("/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="HYP)" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP'" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="FILLING_BP_RATE_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#7"/>
+<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="FILLING_BP_VOLUME_RANGE=0 ‥ 6000" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#*"/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="HYP+" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP)" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="FILLING_BP_VOLUME_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm1"/>
+<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="RINSING_BP_RATE_RANGE=50 ‥ 300" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#,"/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="HYP-" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP+" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="RINSING_BP_RATE_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm2"/>
+<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="DF_FLOW_RANGE=50 ‥ 300" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#."/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="HYP/" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP-" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="DF_FLOW_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm3"/>
+<org.eventb.core.poPredicate name="PRD8" org.eventb.core.predicate="RINSING_TIME_RANGE=0 ‥ 59" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#0"/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="HYP1" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP\/" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD9" org.eventb.core.predicate="RINSING_TIME_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm4"/>
+<org.eventb.core.poPredicate name="PRD10" org.eventb.core.predicate="UF_RINSING_RATE_RANGE=0 ‥ 3000" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#2"/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="HYP3" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP1" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD11" org.eventb.core.predicate="UF_RINSING_RATE_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm5"/>
+<org.eventb.core.poPredicate name="PRD12" org.eventb.core.predicate="UF_RINSING_VOLUME_RANGE=0 ‥ 2950" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#4"/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="HYP5" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP3" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD13" org.eventb.core.predicate="UF_RINSING_VOLUME_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm6"/>
+<org.eventb.core.poPredicate name="PRD14" org.eventb.core.predicate="BLOOD_FLOW_RANGE=50 ‥ 600" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#6"/>
+</org.eventb.core.poPredicateSet>
+<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/HDMachine/c8-rinsing_parameters.bpo|org.eventb.core.poFile#c8-rinsing_parameters|org.eventb.core.poPredicateSet#HYP5" org.eventb.core.poStamp="0">
+<org.eventb.core.poPredicate name="PRD15" org.eventb.core.predicate="BLOOD_FLOW_RANGE≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/HDMachine/c8-rinsing_parameters.buc|org.eventb.core.contextFile#c8-rinsing_parameters|org.eventb.core.axiom#axm7"/>
+</org.eventb.core.poPredicateSet>
+</org.eventb.core.poFile>