c3_outcomes.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="/progmanmodel/c2_modules.bcc|org.eventb.core.scContextFile#c2_modules" org.eventb.core.source="/progmanmodel/c3_outcomes.buc|org.eventb.core.contextFile#c3_outcomes|org.eventb.core.extendsContext#'"/>
<org.eventb.core.scInternalContext name="c0_users">
<org.eventb.core.scCarrierSet name="USER" org.eventb.core.source="/progmanmodel/c0_users.buc|org.eventb.core.contextFile#c0_users|org.eventb.core.carrierSet#_swFc0EHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="c1_programmes">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/progmanmodel/c0_users.bcc|org.eventb.core.scContextFile#c0_users" org.eventb.core.source="/progmanmodel/c1_programmes.buc|org.eventb.core.contextFile#c1_programmes|org.eventb.core.extendsContext#_qcMHkEHSEeqHCPZ-G665YQ"/>
<org.eventb.core.scCarrierSet name="PROGRAMME" org.eventb.core.source="/progmanmodel/c1_programmes.buc|org.eventb.core.contextFile#c1_programmes|org.eventb.core.carrierSet#_qcMuoEHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(PROGRAMME)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="c2_modules">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/progmanmodel/c1_programmes.bcc|org.eventb.core.scContextFile#c1_programmes" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.extendsContext#_fuhrAEHSEeqHCPZ-G665YQ"/>
<org.eventb.core.scAxiom name="c1_programmet" org.eventb.core.label="axm21" org.eventb.core.predicate="credits={15,30,45,60}" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_rGOvUUgCEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="c1_programmeu" org.eventb.core.label="axm22" org.eventb.core.predicate="sum∈(MODULE ↔ credits) → ℕ" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_Ut5fQE5AEeqUxct8tLY9IA" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="c1_programmev" org.eventb.core.label="axm23" org.eventb.core.predicate="sum(∅ ⦂ ℙ(MODULE×ℤ))=0" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_Ut5fQU5AEeqUxct8tLY9IA" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="c1_programmew" org.eventb.core.label="sum24" org.eventb.core.predicate="∀f⦂ℙ(MODULE×ℤ),m⦂MODULE·f∈MODULE ⇸ credits∧m∈dom(f)⇒sum(f)=sum({m} ⩤ f)+f(m)" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_duc5wE5AEeqUxct8tLY9IA" org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="MODULE" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.carrierSet#_fuiSEEHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(MODULE)"/>
<org.eventb.core.scConstant name="credits" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.constant#_rGOvUEgCEeqeqbGZOOBkaQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scConstant name="sum" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.constant#_Ut44ME5AEeqUxct8tLY9IA" org.eventb.core.type="ℙ(ℙ(MODULE×ℤ)×ℤ)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scCarrierSet name="M_OUTCOME" org.eventb.core.source="/progmanmodel/c3_outcomes.buc|org.eventb.core.contextFile#c3_outcomes|org.eventb.core.carrierSet#_HOa80EHTEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(M_OUTCOME)"/>
<org.eventb.core.scCarrierSet name="P_OUTCOME" org.eventb.core.source="/progmanmodel/c3_outcomes.buc|org.eventb.core.contextFile#c3_outcomes|org.eventb.core.carrierSet#_HObj4EHTEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(P_OUTCOME)"/>
</org.eventb.core.scContextFile>