Pattern-Instanciation-On-System-Engineering-Model/Event-B/pseim/mLink.bcm

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;de.prob.units.mchBase;org.eventb.codegen.ui.cgConfig">
<org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/mPort.bcm" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.refinesMachine#_a6WF0MOWEeeQteb5bDCu6g"/>
<org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/cLink.bcc" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.seesContext#_a6WF0cOWEeeQteb5bDCu6g"/>
<org.eventb.core.scInternalContext name="cModel">
<org.eventb.core.scAxiom name="'" org.eventb.core.label="Pattern_ty" org.eventb.core.predicate="Pattern⊆Model" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_h20wcfqkEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="(" org.eventb.core.label="Mdl_ty" org.eventb.core.predicate="Mdl∈Model ∖ Pattern" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_h20wcvqkEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name=")" org.eventb.core.label="Pat_ty" org.eventb.core.predicate="Pat∈Pattern" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_h20wc_qkEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="*" org.eventb.core.label="Inst_ty" org.eventb.core.predicate="Inst∈Model ∖ Pattern" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_fxjdEQKnEeiAPf1wPUl3Gw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="+" org.eventb.core.label="Inst_Mdl" org.eventb.core.predicate="Inst≠Mdl" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_DGgrYAUMEei9ocE08JsPSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="Inst" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.constant#_fxjdEAKnEeiAPf1wPUl3Gw" org.eventb.core.type="Model"/>
<org.eventb.core.scConstant name="Mdl" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.constant#_h20JYPqkEeectLZKwQfI0A" org.eventb.core.type="Model"/>
<org.eventb.core.scCarrierSet name="Model" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.carrierSet#_5dsj0PqTEeectLZKwQfI0A" org.eventb.core.type="ℙ(Model)"/>
<org.eventb.core.scConstant name="Pat" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.constant#_b4aBsPraEeerIsS6OyYQ4w" org.eventb.core.type="Model"/>
<org.eventb.core.scConstant name="Pattern" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.constant#_h20wcPqkEeectLZKwQfI0A" org.eventb.core.type="ℙ(Model)"/>
<org.eventb.core.scCarrierSet name="Property" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.carrierSet#_9dBM4ADlEei-meqqkXX9bA" org.eventb.core.type="ℙ(Property)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="cComponent">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/cModel.bcc|org.eventb.core.scContextFile#cModel" org.eventb.core.source="/MODELS_INC_V9_VAR/cComponent.buc|org.eventb.core.contextFile#cComponent|org.eventb.core.extendsContext#_IT7_UPqUEeectLZKwQfI0A"/>
<org.eventb.core.scCarrierSet name="Component" org.eventb.core.source="/MODELS_INC_V9_VAR/cComponent.buc|org.eventb.core.contextFile#cComponent|org.eventb.core.carrierSet#_IT7_UfqUEeectLZKwQfI0A" org.eventb.core.type="ℙ(Component)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="cPort">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/cComponent.bcc|org.eventb.core.scContextFile#cComponent" org.eventb.core.source="/MODELS_INC_V9_VAR/cPort.buc|org.eventb.core.contextFile#cPort|org.eventb.core.extendsContext#'"/>
<org.eventb.core.scAxiom name="cComponenu" org.eventb.core.label="part" org.eventb.core.predicate="partition(Port,IPort,OPort)" org.eventb.core.source="/MODELS_INC_V9_VAR/cPort.buc|org.eventb.core.contextFile#cPort|org.eventb.core.axiom#_Y1LocvqyEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/cPort.buc|org.eventb.core.contextFile#cPort|org.eventb.core.constant#_Y1LocPqyEeectLZKwQfI0A" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.scConstant name="OPort" org.eventb.core.source="/MODELS_INC_V9_VAR/cPort.buc|org.eventb.core.contextFile#cPort|org.eventb.core.constant#_Y1LocfqyEeectLZKwQfI0A" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.scCarrierSet name="Port" org.eventb.core.source="/MODELS_INC_V9_VAR/cPort.buc|org.eventb.core.contextFile#cPort|org.eventb.core.carrierSet#_YwaNQPqeEeectLZKwQfI0A" org.eventb.core.type="ℙ(Port)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="cLink">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/cPort.bcc|org.eventb.core.scContextFile#cPort" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.extendsContext#'"/>
<org.eventb.core.scAxiom name="cComponenu" org.eventb.core.label="link_k" org.eventb.core.predicate="partition(Link,Transpose,Identity,Shift,First,Rotate)" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.axiom#_u1ZfsfgzEeeeS5KQUtrGlw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="cComponenv" org.eventb.core.label="LKind" org.eventb.core.predicate="LKind={Transpose,Identity,Shift,First,Rotate}" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.axiom#_u1ZfsvgzEeeeS5KQUtrGlw" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="First" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.constant#_WzjhM_g8EeeeS5KQUtrGlw" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.scConstant name="Identity" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.constant#_WzjhMfg8EeeeS5KQUtrGlw" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.scConstant name="LKind" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.constant#_u1ZfsPgzEeeeS5KQUtrGlw" org.eventb.core.type="ℙ(ℙ(Link))"/>
<org.eventb.core.scCarrierSet name="Link" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.carrierSet#_IabHcPoIEeeOzddrJxUeNA" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.scConstant name="Rotate" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.constant#_WzjhNPg8EeeeS5KQUtrGlw" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.scConstant name="Shift" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.constant#_WzjhMvg8EeeeS5KQUtrGlw" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.scConstant name="Transpose" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.constant#_WzjhMPg8EeeeS5KQUtrGlw" org.eventb.core.type="ℙ(Link)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="cComponenu" org.eventb.core.label="comp" org.eventb.core.predicate="components∈Model ↔ Component" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0Y_qUEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponenv" org.eventb.core.label="comp_finite" org.eventb.core.predicate="∀m⦂Model·finite(components[{m}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_cQf0ZPqUEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponenw" org.eventb.core.label="comp_not_shared" org.eventb.core.predicate="components∼∈Component ⇸ Model" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ip9Q0PqUEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponenx" org.eventb.core.label="c_mult" org.eventb.core.predicate="c_multiplicity∈components[{Pat}] → ℕ" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_GMp30PqWEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeny" org.eventb.core.label="cont_ty" org.eventb.core.predicate="container∈ran(components) ⇸ ran(components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8fqgEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponenz" org.eventb.core.label="cl_ty" org.eventb.core.predicate="containers∈ran(components) ↔ ran(components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gmDo8vqgEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponen{" org.eventb.core.label="cl_fin" org.eventb.core.predicate="∀c⦂Component·finite(containers∼[{c}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_oXBHAPqkEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponen|" org.eventb.core.label="cl_cont" org.eventb.core.predicate="container⊆containers" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNI_qkEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponen}" org.eventb.core.label="cl_trans" org.eventb.core.predicate="containers;containers⊆containers" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dqNJPqkEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponen~" org.eventb.core.label="cl_left" org.eventb.core.predicate="containers⊆container;(containers∪(id ⦂ ℙ(Component×Component)))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_1dq0MPqkEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo'" org.eventb.core.label="cl_irrefl" org.eventb.core.predicate="containers∩(id ⦂ ℙ(Component×Component))=(∅ ⦂ ℙ(Component×Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEQA1EeictLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo(" org.eventb.core.label="cl_comp" org.eventb.core.predicate="components;containers;components∼⊆(id ⦂ ℙ(Model×Model))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_l7KVEgA1EeictLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo)" org.eventb.core.label="cl_compr" org.eventb.core.predicate="components;containers∼;components∼⊆(id ⦂ ℙ(Model×Model))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Hwdz4AKtEeiAPf1wPUl3Gw" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeo*" org.eventb.core.label="cont_ctr" org.eventb.core.predicate="components;container;components∼⊆(id ⦂ ℙ(Model×Model))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_xudpYQK5EeiAPf1wPUl3Gw" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeo+" org.eventb.core.label="cont_fin" org.eventb.core.predicate="∀c⦂Component·finite(container∼[{c}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_fxu54ALAEeiAPf1wPUl3Gw" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeo," org.eventb.core.label="irrefl" org.eventb.core.predicate="container∩(id ⦂ ℙ(Component×Component))=(∅ ⦂ ℙ(Component×Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_PaxdoAMwEei9ocE08JsPSw" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeo-" org.eventb.core.label="cont_mono" org.eventb.core.predicate="∀s⦂Component,c⦂Component·s ↦ c∈container⇒containers∼[{s}]⊂containers∼[{c}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_nieoAAMxEei9ocE08JsPSw" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeo." org.eventb.core.label="to_unfold_c_in" org.eventb.core.predicate="to_unfold_c_in∈components[{Pat}] ↔ components[{Inst}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0AMzEei9ocE08JsPSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo/" org.eventb.core.label="to_unfold_c" org.eventb.core.predicate="to_unfold_c⊆components[{Pat}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0QMzEei9ocE08JsPSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo0" org.eventb.core.label="inst2pat_c_ty" org.eventb.core.predicate="inst2pat_c∈components[{Inst}] → components[{Pat}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_gxZD0gMzEei9ocE08JsPSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo1" org.eventb.core.label="inst2pat_unfold_in" org.eventb.core.predicate="to_unfold_c_in;inst2pat_c⊆container" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_V6rHAAM1Eei9ocE08JsPSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo2" org.eventb.core.label="pat2inst_unfold" org.eventb.core.predicate="to_unfold_c∩ran(inst2pat_c)=(∅ ⦂ ℙ(Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_4gspwAkfEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo3" org.eventb.core.label="unfold_root" org.eventb.core.predicate="to_unfold_c∩dom(container)=(∅ ⦂ ℙ(Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ClMccAk_EeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo4" org.eventb.core.label="unfold_in" org.eventb.core.predicate="dom(to_unfold_c_in)⊆dom(container)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_6Bzq0AlZEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo5" org.eventb.core.label="unfold_mul" org.eventb.core.predicate="∀c⦂Component·c∈to_unfold_c⇒c_multiplicity(c)&gt;0" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_-v2gwAl5EeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo6" org.eventb.core.label="unfold_in_mul" org.eventb.core.predicate="∀c⦂Component·c∈dom(to_unfold_c_in)⇒c_multiplicity(c)&gt;0" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_Ar4dsAl8EeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo7" org.eventb.core.label="unfold_in_i2p" org.eventb.core.predicate="ran(to_unfold_c_in)⊆dom(inst2pat_c)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_byYtUAxjEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo8" org.eventb.core.label="unfold_cont" org.eventb.core.predicate="(inst2pat_c;to_unfold_c_in)∩container=(∅ ⦂ ℙ(Component×Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ptqDcQxlEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo9" org.eventb.core.label="unfold_unfold_in" org.eventb.core.predicate="to_unfold_c∩dom(to_unfold_c_in)=(∅ ⦂ ℙ(Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_ptqDcgxlEeqU6uo9ksjEPA" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeo:" org.eventb.core.label="unfold_fin" org.eventb.core.predicate="∀c⦂Component·finite(to_unfold_c_in[{c}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_MM724AxtEeqU6uo9ksjEPA" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeo;" org.eventb.core.label="inst2pat_cont" org.eventb.core.predicate="inst2pat_c;container=container;inst2pat_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_MM724QxtEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo=" org.eventb.core.label="c_index_ty" org.eventb.core.predicate="c_index∈dom(inst2pat_c) → ℕ" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#__R1F0QyBEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo&gt;" org.eventb.core.label="to_clone_c_mult" org.eventb.core.predicate="∀c⦂Component·c∈dom(inst2pat_c)⇒c_index(c)∈1 ‥ c_multiplicity(inst2pat_c(c))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_nEDgcg3EEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo?" org.eventb.core.label="M_fin" org.eventb.core.predicate="finite(ran(c_multiplicity))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_nEDgcw3EEeqU6uo9ksjEPA" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeo@" org.eventb.core.label="P" org.eventb.core.predicate="P=components[{Pat}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_nEDgdA3EEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoA" org.eventb.core.label="Pnz" org.eventb.core.predicate="P≠(∅ ⦂ ℙ(Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_nEDgdQ3EEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoB" org.eventb.core.label="M" org.eventb.core.predicate="M=max(ran(c_multiplicity))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_3N038Q6WEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoC" org.eventb.core.label="P_fin" org.eventb.core.predicate="finite(P)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_rcyHQA6gEeqU6uo9ksjEPA" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeoD" org.eventb.core.label="c_indexes_ty" org.eventb.core.predicate="c_indexes∈dom(inst2pat_c) ↣ (P ⇸ 1 ‥ M)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_rcyHQQ6gEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoE" org.eventb.core.label="c_indexes_dom" org.eventb.core.predicate="∀i⦂Component·i∈dom(inst2pat_c)⇒dom(c_indexes(i))=(containers∪(id ⦂ ℙ(Component×Component)))[{inst2pat_c(i)}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_2SMx0Q7FEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoF" org.eventb.core.label="c_indexes_val" org.eventb.core.predicate="∀i⦂Component·i∈dom(inst2pat_c)⇒c_indexes(i)=inst2pat_c∼;((containers∪(id ⦂ ℙ(Component×Component)))[{i}] ◁ c_index)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_2SMx0g7FEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoG" org.eventb.core.label="i2p_dom" org.eventb.core.predicate="∀i⦂Component·i∈dom(inst2pat_c)⇒containers[{i}]⊆dom(inst2pat_c)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_2SMx0w7FEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoH" org.eventb.core.label="unfold_index_ext" org.eventb.core.predicate="∀c⦂Component,m⦂ℙ(Component×ℤ)·c∈to_unfold_c∧m∈ran(c_indexes)⇒c∉dom(m)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_2SMx1A7FEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoI" org.eventb.core.label="unfold_in_index_ext" org.eventb.core.predicate="∀c⦂Component,i⦂Component,m⦂ℙ(Component×ℤ)·c ↦ i∈to_unfold_c_in∧c_indexes(i)⊆m∧m∈ran(c_indexes)⇒c∉dom(m)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_iR6UgA7fEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoJ" org.eventb.core.label="unfold_index" org.eventb.core.predicate="∀c⦂Component,k⦂ℤ·c∈to_unfold_c∧k∈1 ‥ M⇒{c ↦ k}∉ran(c_indexes)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_BSFPUBEBEeqU6uo9ksjEPA" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeoK" org.eventb.core.label="unfold_in_index" org.eventb.core.predicate="∀c⦂Component,i⦂Component,k⦂ℤ·c ↦ i∈to_unfold_c_in∧k∈1 ‥ M⇒c_indexes(i){c ↦ k}∉ran(c_indexes)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.invariant#_vsdVYCC3Eeq7BuY4D8yZpw" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="cComponeoL" org.eventb.core.label="prop" org.eventb.core.predicate="cProperties∈Component ↔ Property" org.eventb.core.source="/MODELS_INC_V9_VAR/mProperty.bum|org.eventb.core.machineFile#mProperty|org.eventb.core.invariant#_0kf_RPqeEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoM" org.eventb.core.label="port" org.eventb.core.predicate="ports∈ran(components) ↔ Port" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_0kf_RPqeEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoN" org.eventb.core.label="port_finite" org.eventb.core.predicate="∀c⦂Component·finite(ports[{c}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_0kf_RfqeEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoO" org.eventb.core.label="port_not_shared" org.eventb.core.predicate="ports∼∈Port ⇸ Component" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_0kf_RvqeEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoP" org.eventb.core.label="p_mult" org.eventb.core.predicate="p_multiplicity∈(components;ports)[Pattern] → ℕ" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_0kf_R_qeEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoQ" org.eventb.core.label="to_unfold_p_in" org.eventb.core.predicate="to_unfold_p_in∈(components;ports)[{Pat}] ↔ components[{Inst}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_btIX4vqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoR" org.eventb.core.label="inst2pat_p_ty" org.eventb.core.predicate="inst2pat_p∈(components;ports)[{Inst}] → (components;ports)[{Pat}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_zYW3EfqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoS" org.eventb.core.label="inst2pat_commp" org.eventb.core.predicate="inst2pat_p;ports∼=ports∼;inst2pat_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_F0IYkPriEeerIsS6OyYQ4w" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoT" org.eventb.core.label="to_unfold_p_inst2pat" org.eventb.core.predicate="ran(to_unfold_p_in)⊆dom(inst2pat_c)" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_ui7VEAFGEei9ocE08JsPSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoU" org.eventb.core.label="to_unfold_p_in_comp" org.eventb.core.predicate="to_unfold_p_in;inst2pat_c⊆ports∼" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_zY448gK7EeiAPf1wPUl3Gw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoV" org.eventb.core.label="i2p_IPort" org.eventb.core.predicate="inst2pat_p[IPort]⊆IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_22_TUALCEeiAPf1wPUl3Gw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoW" org.eventb.core.label="i2p_OPort" org.eventb.core.predicate="inst2pat_p[OPort]⊆OPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_QFUfMAWQEei9ocE08JsPSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoX" org.eventb.core.label="p_index_ty" org.eventb.core.predicate="p_index∈dom(inst2pat_p) → ℕ" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.invariant#_QFVGQAWQEei9ocE08JsPSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoY" org.eventb.core.label="link_ty" org.eventb.core.predicate="links∈ran(components) ↔ Link" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_S_fWR74_EeeN0675uvquSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoZ" org.eventb.core.label="link_finite" org.eventb.core.predicate="∀c⦂Component·finite(links[{c}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_S_fWSL4_EeeN0675uvquSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo[" org.eventb.core.label="link_not_shared" org.eventb.core.predicate="links∼∈Link ⇸ Component" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_S_f9UL4_EeeN0675uvquSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo\" org.eventb.core.label="src_ty" org.eventb.core.predicate="src∈ran(links) → ran(ports)" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_S_f9Ub4_EeeN0675uvquSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo]" org.eventb.core.label="dst_ty" org.eventb.core.predicate="dst∈ran(links) → ran(ports)" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_S_f9Ur4_EeeN0675uvquSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo^" org.eventb.core.label="link_cii" org.eventb.core.predicate="links;((src ⊗ dst) ▷ (IPort × IPort))⊆ports ⊗ (container∼;ports)" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_0ffzssOZEeeQteb5bDCu6g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo_" org.eventb.core.label="link_coi" org.eventb.core.predicate="links;((src ⊗ dst) ▷ (OPort × IPort))⊆(container∼;ports) ⊗ (container∼;ports)" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_Z5iv0vg-EeeeS5KQUtrGlw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeo`" org.eventb.core.label="link_coo" org.eventb.core.predicate="links;((src ⊗ dst) ▷ (OPort × OPort))⊆(container∼;ports) ⊗ ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_GNeQ0_qOEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoa" org.eventb.core.label="link_cio" org.eventb.core.predicate="links;((src ⊗ dst) ▷ (IPort × OPort))⊆ports ⊗ ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_GNe34PqOEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeob" org.eventb.core.label="transp_src" org.eventb.core.predicate="∀l⦂Link·l∈(components;links)[{Pat}]∩Transpose⇒p_multiplicity(src(l))=c_multiplicity(ports∼(dst(l)))" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_69ZZAPq0EeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoc" org.eventb.core.label="transp_dst" org.eventb.core.predicate="∀l⦂Link·l∈(components;links)[{Pat}]∩Transpose⇒p_multiplicity(dst(l))=c_multiplicity(ports∼(src(l)))" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_X1DEFAA3EeictLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeod" org.eventb.core.label="c_links_done" org.eventb.core.predicate="c_links_done⊆(components;links)[{Pat}] × components[{Inst}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_ocRYQAbKEeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoe" org.eventb.core.label="inst2pat_l_ty" org.eventb.core.predicate="inst2pat_l∈(components;links)[{Inst}] → (components;links)[{Pat}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_ocRYQQbKEeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeof" org.eventb.core.label="inst2pat_l_preserve_type" org.eventb.core.predicate="∀K⦂ℙ(Link)·K∈LKind⇒inst2pat_l[K]⊆K" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_cztlsQi3EeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeog" org.eventb.core.label="inst2pat_l_src" org.eventb.core.predicate="inst2pat_l;src=src;inst2pat_p" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_rQxpAQskEeigQsLVMUeRQw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoh" org.eventb.core.label="inst2pat_l_dst" org.eventb.core.predicate="inst2pat_l;dst=dst;inst2pat_p" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_rQxpAgskEeigQsLVMUeRQw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoi" org.eventb.core.label="transp_correct1" org.eventb.core.predicate="∀l⦂Link·l∈(components;links)[{Inst}]∩Transpose⇒p_index(src(l))=c_index(ports∼(dst(l)))" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_EviiYAslEeigQsLVMUeRQw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="cComponeoj" org.eventb.core.label="transp_correct2" org.eventb.core.predicate="∀l⦂Link·l∈(components;links)[{Inst}]∩Transpose⇒p_index(dst(l))=c_index(ports∼(src(l)))" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.invariant#_EviiYQslEeigQsLVMUeRQw" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="M" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_QZUfgOTyEeemadOWCHlIvw" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="P" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_QZUfgeTyEeemadOWCHlIvw" org.eventb.core.type="ℙ(Component)"/>
<org.eventb.core.scVariable name="cProperties" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_Z5iv0fg-EeeeS5KQUtrGlw" org.eventb.core.type="ℙ(Component×Property)"/>
<org.eventb.core.scVariable name="c_index" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_73nGMMOYEeeQteb5bDCu6g" org.eventb.core.type="ℙ(Component×ℤ)"/>
<org.eventb.core.scVariable name="c_indexes" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_Z5iv0Pg-EeeeS5KQUtrGlw" org.eventb.core.type="ℙ(Component×ℙ(Component×ℤ))"/>
<org.eventb.core.scVariable name="c_links_done" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_K9xMMRKbEeqU6uo9ksjEPA" org.eventb.core.type="ℙ(Link×Component)"/>
<org.eventb.core.scVariable name="c_multiplicity" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_S_fWRr4_EeeN0675uvquSw" org.eventb.core.type="ℙ(Component×ℤ)"/>
<org.eventb.core.scVariable name="components" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_S_fWQr4_EeeN0675uvquSw" org.eventb.core.type="ℙ(Model×Component)"/>
<org.eventb.core.scVariable name="container" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_S_fWRL4_EeeN0675uvquSw" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.scVariable name="containers" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_S_fWRb4_EeeN0675uvquSw" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.scVariable name="dst" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_K9xMMBKbEeqU6uo9ksjEPA" org.eventb.core.type="ℙ(Link×Port)"/>
<org.eventb.core.scVariable name="inst2pat_c" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_j2NdQeGVEeeUoZak4Ibgcg" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.scVariable name="inst2pat_l" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_K9xMMhKbEeqU6uo9ksjEPA" org.eventb.core.type="ℙ(Link×Link)"/>
<org.eventb.core.scVariable name="inst2pat_p" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_X1DEEwA3EeictLZKwQfI0A" org.eventb.core.type="ℙ(Port×Port)"/>
<org.eventb.core.scVariable name="links" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_cztlsAi3EeiFlqW-8GKglg" org.eventb.core.type="ℙ(Component×Link)"/>
<org.eventb.core.scVariable name="p_index" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_X1DEEQA3EeictLZKwQfI0A" org.eventb.core.type="ℙ(Port×ℤ)"/>
<org.eventb.core.scVariable name="p_multiplicity" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_X1DEEAA3EeictLZKwQfI0A" org.eventb.core.type="ℙ(Port×ℤ)"/>
<org.eventb.core.scVariable name="ports" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_Ajk8sPloEeeeS5KQUtrGlw" org.eventb.core.type="ℙ(Component×Port)"/>
<org.eventb.core.scVariable name="src" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_rQxpAAskEeigQsLVMUeRQw" org.eventb.core.type="ℙ(Link×Port)"/>
<org.eventb.core.scVariable name="to_unfold_c" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_0ffzsMOZEeeQteb5bDCu6g" org.eventb.core.type="ℙ(Component)"/>
<org.eventb.core.scVariable name="to_unfold_c_in" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_j2NdQOGVEeeUoZak4Ibgcg" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.scVariable name="to_unfold_p_in" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variable#_X1DEEgA3EeictLZKwQfI0A" org.eventb.core.type="ℙ(Port×Component)"/>
<org.eventb.core.scVariant name="to_unfold_p_io" org.eventb.core.expression="((components;links)[{Pat}] × components[{Inst}]) ∖ c_links_done" org.eventb.core.label="VARIANT" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.variant#_K8id4Ai5EeiFlqW-8GKglg"/>
<org.eventb.core.scEvent name="to_unfold_p_ip" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="instanciate_pattern" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/mPort.bcm|org.eventb.core.scMachineFile#mPort|org.eventb.core.scEvent#to_unfold_p_ip" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'|org.eventb.core.refinesEvent#_ypF-0PlnEeeeS5KQUtrGlw"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="ic" org.eventb.core.predicate="inst_components∈components[{Pat}] ↔ components[{Mdl}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.guard#_O1UjgvqmEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="icr" org.eventb.core.predicate="inst_components∼∈components[{Mdl}] ⇸ components[{Pat}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.guard#_O1Ujg_qmEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="cm" org.eventb.core.predicate="c_mult_others∈components[{Pat}] ∖ dom(inst_components) → ℕ" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.guard#_O1UjhPqmEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="cmult" org.eventb.core.predicate="c_mult=c_mult_others{pc⦂Component·pc∈dom(inst_components) ∣ pc ↦ card(inst_components[{pc}])}" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.guard#_O1WYsfqmEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_component~" org.eventb.core.label="ip" org.eventb.core.predicate="inst_ports∈(components;ports)[{Pat}] ↔ (components;ports)[{Mdl}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.guard#_btHw0_qwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu'" org.eventb.core.label="ipr" org.eventb.core.predicate="inst_ports∼∈(components;ports)[{Mdl}] ⇸ (components;ports)[{Pat}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.guard#_btHw1PqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu(" org.eventb.core.label="pm" org.eventb.core.predicate="p_mult_others∈(components;ports)[{Pat}] ∖ dom(inst_ports) → ℕ" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.guard#_btHw1fqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu)" org.eventb.core.label="thm" org.eventb.core.predicate="∀p⦂Port·finite(inst_ports[{p}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.guard#_btHw1vqwEeectLZKwQfI0A" org.eventb.core.theorem="true"/>
<org.eventb.core.scAction name="inst_componentt" org.eventb.core.assignment="c_multiplicity ≔ c_mult" org.eventb.core.label="c_mult" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1UjhfqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componentu" org.eventb.core.assignment="to_unfold_c ≔ (components[{Pat}] ∖ dom(container)) ∖ c_mult∼[{0}]" org.eventb.core.label="to_unfold_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1WYt_qmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componentv" org.eventb.core.assignment="to_unfold_c_in ≔ ∅ ⦂ ℙ(Component×Component)" org.eventb.core.label="to_unfold_c_in" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1WYuPqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componentw" org.eventb.core.assignment="components ≔ {Inst} ⩤ components" org.eventb.core.label="components_inst" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1W_xPqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componentx" org.eventb.core.assignment="container ≔ components[{Inst}] ⩤ container" org.eventb.core.label="container_inst" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1W_xfqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componenty" org.eventb.core.assignment="containers ≔ components[{Inst}] ⩤ containers" org.eventb.core.label="containers_inst" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1W_xvqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componentz" org.eventb.core.assignment="c_index ≔ ∅ ⦂ ℙ(Component×ℤ)" org.eventb.core.label="c_index" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1W_x_qmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_component{" org.eventb.core.assignment="c_indexes ≔ ∅ ⦂ ℙ(Component×ℙ(Component×ℤ))" org.eventb.core.label="c_indexes" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1W_yPqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_component|" org.eventb.core.assignment="inst2pat_c ≔ ∅ ⦂ ℙ(Component×Component)" org.eventb.core.label="pat2inst_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1Xm1PqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_component}" org.eventb.core.assignment="M ≔ max(ran(c_mult))" org.eventb.core.label="M" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.action#_O1Xm1fqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componenu*" org.eventb.core.assignment="p_multiplicity ≔ p_multiplicity(p_mult_others{pp⦂Port·pp∈(components;ports)[{Pat}] ∣ pp ↦ card(inst_ports[{pp}])})" org.eventb.core.label="p_mult" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.action#_btIX4PqwEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componenu+" org.eventb.core.assignment="inst2pat_p ≔ ∅ ⦂ ℙ(Port×Port)" org.eventb.core.label="inst2pat_p" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.action#_btJmA_qwEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componenu," org.eventb.core.assignment="ports ≔ components[{Inst}] ⩤ ports" org.eventb.core.label="ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.action#_btJmCfqwEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componenu-" org.eventb.core.assignment="to_unfold_p_in ≔ ∅ ⦂ ℙ(Port×Component)" org.eventb.core.label="unfold_p" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.action#_btJmCvqwEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="inst_componenu." org.eventb.core.assignment="p_index ≔ ∅ ⦂ ℙ(Port×ℤ)" org.eventb.core.label="p_index" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.action#_btKNEPqwEeectLZKwQfI0A"/>
<org.eventb.core.scParameter name="c_mult" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.parameter#_O1VxofqmEeectLZKwQfI0A" org.eventb.core.type="ℙ(Component×ℤ)"/>
<org.eventb.core.scParameter name="c_mult_others" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.parameter#_O1UjgfqmEeectLZKwQfI0A" org.eventb.core.type="ℙ(Component×ℤ)"/>
<org.eventb.core.scParameter name="inst_components" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#'|org.eventb.core.parameter#_O1UjgPqmEeectLZKwQfI0A" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.scParameter name="inst_ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.parameter#_btHw0fqwEeectLZKwQfI0A" org.eventb.core.type="ℙ(Port×Port)"/>
<org.eventb.core.scParameter name="p_mult_others" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#'|org.eventb.core.parameter#_btHw0vqwEeectLZKwQfI0A" org.eventb.core.type="ℙ(Port×ℤ)"/>
<org.eventb.core.scGuard name="inst_componenu/" org.eventb.core.label="transp_ctr1" org.eventb.core.predicate="∀l⦂Link·l∈(components;links)[{Pat}]∩Transpose∧ports∼(dst(l))∈dom(inst_components)⇒card(inst_ports[{src(l)}])=card(inst_components[{ports∼(dst(l))}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'|org.eventb.core.guard#_S_eIJL4_EeeN0675uvquSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu0" org.eventb.core.label="transp_ctr2" org.eventb.core.predicate="∀l⦂Link·l∈(components;links)[{Pat}]∩Transpose∧ports∼(dst(l))∉dom(inst_components)⇒card(inst_ports[{src(l)}])=c_mult_others(ports∼(dst(l)))" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'|org.eventb.core.guard#_S_eIJb4_EeeN0675uvquSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu1" org.eventb.core.label="transp_ctr3" org.eventb.core.predicate="∀l⦂Link·l∈(components;links)[{Pat}]∩Transpose∧ports∼(src(l))∈dom(inst_components)⇒card(inst_ports[{dst(l)}])=card(inst_components[{ports∼(src(l))}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'|org.eventb.core.guard#_S_eIJr4_EeeN0675uvquSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu2" org.eventb.core.label="transp_ctr4" org.eventb.core.predicate="∀l⦂Link·l∈(components;links)[{Pat}]∩Transpose∧ports∼(src(l))∉dom(inst_components)⇒card(inst_ports[{dst(l)}])=c_mult_others(ports∼(src(l)))" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'|org.eventb.core.guard#_S_eIJ74_EeeN0675uvquSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="inst_componenu3" org.eventb.core.assignment="links ≔ components[{Inst}] ⩤ links" org.eventb.core.label="links" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'|org.eventb.core.action#_S_evNr4_EeeN0675uvquSw"/>
<org.eventb.core.scAction name="inst_componenu4" org.eventb.core.assignment="src ≔ (components;links)[{Inst}] ⩤ src" org.eventb.core.label="src" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'|org.eventb.core.action#_oe6yMMOjEeeQteb5bDCu6g"/>
<org.eventb.core.scAction name="inst_componenu5" org.eventb.core.assignment="dst ≔ (components;links)[{Inst}] ⩤ dst" org.eventb.core.label="dst" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'|org.eventb.core.action#_oe6yMcOjEeeQteb5bDCu6g"/>
<org.eventb.core.scAction name="inst_componenu6" org.eventb.core.assignment="inst2pat_l ≔ ∅ ⦂ ℙ(Link×Link)" org.eventb.core.label="inst2pat_l" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'|org.eventb.core.action#_0IWfoAK-EeiAPf1wPUl3Gw"/>
<org.eventb.core.scAction name="inst_componenu7" org.eventb.core.assignment="c_links_done ≔ ∅ ⦂ ℙ(Link×Component)" org.eventb.core.label="c_links_done" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#'|org.eventb.core.action#_SwNs4ALXEei9ocE08JsPSw"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="to_unfold_p_iq" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unfold_root_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_JZbnAOGWEeeUoZak4Ibgcg">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/mPort.bcm|org.eventb.core.scMachineFile#mPort|org.eventb.core.scEvent#to_unfold_p_iq" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_JZbnAOGWEeeUoZak4Ibgcg|org.eventb.core.refinesEvent#_7XcAsAK3EeiAPf1wPUl3Gw"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="c_ty" org.eventb.core.predicate="c∈to_unfold_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYsvqmEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="new_c_ty" org.eventb.core.predicate="new_c∈1 ‥ c_multiplicity(c) ↣ Component ∖ ran(components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYs_qmEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="new_c_fin" org.eventb.core.predicate="finite(ran(new_c))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYtPqmEeectLZKwQfI0A" org.eventb.core.theorem="true"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="new_c_card" org.eventb.core.predicate="card(ran(new_c))=c_multiplicity(c)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYtfqmEeectLZKwQfI0A" org.eventb.core.theorem="true"/>
<org.eventb.core.scAction name="new_d" org.eventb.core.assignment="components ≔ components∪({Inst} × ran(new_c))" org.eventb.core.label="new_c_model" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.action#_O1Xm1vqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="new_e" org.eventb.core.assignment="to_unfold_c_in ≔ to_unfold_c_in∪((container∼[{c}] ∖ c_multiplicity∼[{0}]) × ran(new_c))" org.eventb.core.label="to_unfold_c_in" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.action#_O1Xm1_qmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="new_f" org.eventb.core.assignment="c_index ≔ c_index∪new_c∼" org.eventb.core.label="c_index" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.action#_O1YN4PqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="new_g" org.eventb.core.assignment="to_unfold_c ≔ to_unfold_c ∖ {c}" org.eventb.core.label="to_unfold_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.action#_O1YN4fqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="new_h" org.eventb.core.assignment="inst2pat_c ≔ inst2pat_c∪(ran(new_c) × {c})" org.eventb.core.label="pat2inst_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.action#_O1YN4vqmEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="new_i" org.eventb.core.assignment="c_indexes ≔ c_indexes∪{i⦂Component·i∈ran(new_c) ∣ i ↦ {c ↦ new_c∼(i)}}" org.eventb.core.label="c_indexes" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.action#_lyJKIPreEeerIsS6OyYQ4w"/>
<org.eventb.core.scAction name="new_j" org.eventb.core.assignment="cProperties ≔ cProperties∪(ran(new_c) × cProperties[{c}])" org.eventb.core.label="prop" org.eventb.core.source="/MODELS_INC_V9_VAR/mProperty.bum|org.eventb.core.machineFile#mProperty|org.eventb.core.event#_btIX4_qwEeectLZKwQfI0A|org.eventb.core.action#_btIX4PqwEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="new_k" org.eventb.core.assignment="to_unfold_p_in ≔ to_unfold_p_in∪(ports[{c}] × ran(new_c))" org.eventb.core.label="unfold_p_in" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btIX4_qwEeectLZKwQfI0A|org.eventb.core.action#_btKNFfqwEeectLZKwQfI0A"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.parameter#_O1WYsPqmEeectLZKwQfI0A" org.eventb.core.type="Component"/>
<org.eventb.core.scParameter name="new_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1VxoPqmEeectLZKwQfI0A|org.eventb.core.parameter#_O1W_wPqmEeectLZKwQfI0A" org.eventb.core.type="ℙ(ℤ×Component)"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="to_unfold_p_ir" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unfold_p" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_QZUfguTyEeemadOWCHlIvw">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/mPort.bcm|org.eventb.core.scMachineFile#mPort|org.eventb.core.scEvent#to_unfold_p_is" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_QZUfguTyEeemadOWCHlIvw|org.eventb.core.refinesEvent#_-RPi0P06Eees7pYemx4WBQ"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="p_ty" org.eventb.core.predicate="p ↦ c∈to_unfold_p_in" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.guard#_btHw1_qwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="new_p_ty" org.eventb.core.predicate="new_p∈1 ‥ p_multiplicity(p) ↣ Port ∖ ran(components;ports)" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.guard#_btHw2PqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="duplicate_IPorts_direction" org.eventb.core.predicate="p∈IPort⇒ran(new_p)⊆IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.guard#_btHw2fqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="duplicate_OPorts_direction" org.eventb.core.predicate="p∈OPort⇒ran(new_p)⊆OPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.guard#_btI-8_qwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="new_q" org.eventb.core.assignment="ports ≔ ports∪({c} × ran(new_p))" org.eventb.core.label="new_p_component" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.action#_YHf5cAUuEei9ocE08JsPSw"/>
<org.eventb.core.scAction name="new_r" org.eventb.core.assignment="to_unfold_p_in ≔ to_unfold_p_in ∖ {p ↦ c}" org.eventb.core.label="dp" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.action#_YHiVsAUuEei9ocE08JsPSw"/>
<org.eventb.core.scAction name="new_s" org.eventb.core.assignment="inst2pat_p ≔ inst2pat_p∪(ran(new_p) × {p})" org.eventb.core.label="inst2pat_p" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.action#_YHiVsQUuEei9ocE08JsPSw"/>
<org.eventb.core.scAction name="new_t" org.eventb.core.assignment="p_index ≔ p_index∪new_p∼" org.eventb.core.label="p_index" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.action#_f2PGEAspEeigQsLVMUeRQw"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.parameter#_btI-8vqwEeectLZKwQfI0A" org.eventb.core.type="Component"/>
<org.eventb.core.scParameter name="new_p" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.parameter#_btJmB_qwEeectLZKwQfI0A" org.eventb.core.type="ℙ(ℤ×Port)"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.parameter#_btI-8fqwEeectLZKwQfI0A" org.eventb.core.type="Port"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="to_unfold_p_is" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unfold_node_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_QZVGk-TyEeemadOWCHlIvw">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/mPort.bcm|org.eventb.core.scMachineFile#mPort|org.eventb.core.scEvent#to_unfold_p_ir" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_QZVGk-TyEeemadOWCHlIvw|org.eventb.core.refinesEvent#_K9uI4BKbEeqU6uo9ksjEPA"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="c_ty" org.eventb.core.predicate="c ↦ dest∈to_unfold_c_in" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.guard#_O1WYtvqmEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="new_c_ty" org.eventb.core.predicate="new_c∈1 ‥ c_multiplicity(c) ↣ Component ∖ ran(components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.guard#_O1W_wvqmEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="new_c_fin" org.eventb.core.predicate="finite(ran(new_c))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.guard#_O1W_w_qmEeectLZKwQfI0A" org.eventb.core.theorem="true"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="new_c_card" org.eventb.core.predicate="card(ran(new_c))=c_multiplicity(c)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.guard#_O1Xm0vqmEeectLZKwQfI0A" org.eventb.core.theorem="true"/>
<org.eventb.core.scAction name="new_d" org.eventb.core.assignment="components ≔ components∪({Inst} × ran(new_c))" org.eventb.core.label="new_c_model" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.action#_rQ0PgftxEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="new_e" org.eventb.core.assignment="container ≔ container∪(ran(new_c) × {dest})" org.eventb.core.label="new_c_container" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.action#_xQWRoP01EeeINffjS36taQ"/>
<org.eventb.core.scAction name="new_f" org.eventb.core.assignment="c_index ≔ c_index∪new_c∼" org.eventb.core.label="c_index" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.action#_254qkAA2EeictLZKwQfI0A"/>
<org.eventb.core.scAction name="new_g" org.eventb.core.assignment="to_unfold_c_in ≔ (to_unfold_c_in ∖ {c ↦ dest})∪((container∼[{c}] ∖ c_multiplicity∼[{0}]) × ran(new_c))" org.eventb.core.label="to_unfold_c_in" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.action#_ptpcYAxlEeqU6uo9ksjEPA"/>
<org.eventb.core.scAction name="new_h" org.eventb.core.assignment="inst2pat_c ≔ inst2pat_c∪(ran(new_c) × {c})" org.eventb.core.label="pat2inst_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.action#_ptpcYQxlEeqU6uo9ksjEPA"/>
<org.eventb.core.scAction name="new_i" org.eventb.core.assignment="containers ≔ containers∪(ran(new_c) × {dest})∪(ran(new_c) × containers[{dest}])" org.eventb.core.label="cont" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.action#_ptpcYgxlEeqU6uo9ksjEPA"/>
<org.eventb.core.scAction name="new_j" org.eventb.core.assignment="c_indexes ≔ c_indexes∪{i⦂Component·i∈ran(new_c) ∣ i ↦ c_indexes(dest){c ↦ new_c∼(i)}}" org.eventb.core.label="c_indexes" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.action#__Rz3sAyBEeqU6uo9ksjEPA"/>
<org.eventb.core.scAction name="new_k" org.eventb.core.assignment="cProperties ≔ cProperties∪(ran(new_c) × cProperties[{c}])" org.eventb.core.label="prop" org.eventb.core.source="/MODELS_INC_V9_VAR/mProperty.bum|org.eventb.core.machineFile#mProperty|org.eventb.core.event#_btJmBfqwEeectLZKwQfI0A|org.eventb.core.action#_btJmA_qwEeectLZKwQfI0A"/>
<org.eventb.core.scAction name="new_l" org.eventb.core.assignment="to_unfold_p_in ≔ to_unfold_p_in∪(ports[{c}] × ran(new_c))" org.eventb.core.label="unfold_p_in" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btJmBfqwEeectLZKwQfI0A|org.eventb.core.action#_GO3gcAK8EeiAPf1wPUl3Gw"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.parameter#_O1W_wfqmEeectLZKwQfI0A" org.eventb.core.type="Component"/>
<org.eventb.core.scParameter name="dest" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.parameter#_O1Xm0PqmEeectLZKwQfI0A" org.eventb.core.type="Component"/>
<org.eventb.core.scParameter name="new_c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1WYufqmEeectLZKwQfI0A|org.eventb.core.parameter#_O1Xm0fqmEeectLZKwQfI0A" org.eventb.core.type="ℙ(ℤ×Component)"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="to_unfold_p_it" org.eventb.core.accurate="true" org.eventb.core.convergence="1" org.eventb.core.extended="false" org.eventb.core.label="unfold_node_link_oi_Transpose" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw">
<org.eventb.core.scGuard name="'" org.eventb.core.label="l_ty" org.eventb.core.predicate="l∈(components;links)[{Pat}]∩Transpose" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_JZbnBOGWEeeUoZak4Ibgcg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="src_o" org.eventb.core.predicate="src(l)∈OPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_nOhFweGpEeeUoZak4Ibgcg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="dst_i" org.eventb.core.predicate="dst(l)∈IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_yq8FweGpEeeUoZak4Ibgcg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="c" org.eventb.core.predicate="c∈components[{Inst}]∩dom(inst2pat_c)" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_3EQ2ceGpEeeUoZak4Ibgcg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="not_done" org.eventb.core.predicate="l ↦ c∉c_links_done" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_RYtJ0uT7EeemadOWCHlIvw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="sci" org.eventb.core.predicate="sci∈1 ‥ c_multiplicity(ports∼(src(l))) ↣ container∼[{c}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_RYtJ0-T7EeemadOWCHlIvw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="sci_ctr" org.eventb.core.predicate="inst2pat_c[ran(sci)]⊆{ports∼(src(l))}" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_RYtJ1OT7EeemadOWCHlIvw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="sci_c_index" org.eventb.core.predicate="sci;c_index=(id ⦂ ℙ(ℤ×ℤ))" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_RYtJ1eT7EeemadOWCHlIvw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="/" org.eventb.core.label="dci" org.eventb.core.predicate="dci∈1 ‥ c_multiplicity(ports∼(dst(l))) ↣ container∼[{c}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_WfAcMAK-EeiAPf1wPUl3Gw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="0" org.eventb.core.label="dci_ctr" org.eventb.core.predicate="inst2pat_c[ran(dci)]⊆{ports∼(dst(l))}" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_nHJTNQRrEei9ocE08JsPSw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="1" org.eventb.core.label="dci_c_index" org.eventb.core.predicate="dci;c_index=(id ⦂ ℙ(ℤ×ℤ))" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_DdBJsAc3EeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="2" org.eventb.core.label="spi_ty" org.eventb.core.predicate="spi∈ran(sci) → (1 ‥ p_multiplicity(src(l)) ↣ inst2pat_p∼[{src(l)}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_70QzIAc3EeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="3" org.eventb.core.label="spi_ctr" org.eventb.core.predicate="∀ci⦂Component·ci∈ran(sci)⇒spi(ci)∈1 ‥ p_multiplicity(src(l)) ↣ ports[{ci}]∩OPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_6bPz8AdGEeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="4" org.eventb.core.label="spi_p_index" org.eventb.core.predicate="∀ci⦂Component·ci∈ran(sci)⇒spi(ci);p_index=(id ⦂ ℙ(ℤ×ℤ))" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_6bPz8QdGEeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="5" org.eventb.core.label="dpi_ty" org.eventb.core.predicate="dpi∈ran(dci) → (1 ‥ p_multiplicity(dst(l)) ↣ inst2pat_p∼[{dst(l)}])" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_nxuuQQi-EeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="6" org.eventb.core.label="dpi_ctr" org.eventb.core.predicate="∀ci⦂Component·ci∈ran(dci)⇒dpi(ci)∈1 ‥ p_multiplicity(dst(l)) ↣ ports[{ci}]∩IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_quOpsAjAEeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="7" org.eventb.core.label="dpi_p_index" org.eventb.core.predicate="∀ci⦂Component·ci∈ran(dci)⇒dpi(ci);p_index=(id ⦂ ℙ(ℤ×ℤ))" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_BL1LoAkjEeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="8" org.eventb.core.label="new_l_ty" org.eventb.core.predicate="new_l∈1 ‥ p_multiplicity(src(l)) × 1 ‥ c_multiplicity(ports∼(src(l))) ↣ Transpose ∖ ran(links)" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.guard#_BL1ysAkjEeiFlqW-8GKglg" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.parameter#_nHJTMARrEei9ocE08JsPSw" org.eventb.core.type="Component"/>
<org.eventb.core.scParameter name="dci" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.parameter#_nOhFwOGpEeeUoZak4Ibgcg" org.eventb.core.type="ℙ(ℤ×Component)"/>
<org.eventb.core.scParameter name="dpi" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.parameter#_JZbnAuGWEeeUoZak4Ibgcg" org.eventb.core.type="ℙ(Component×ℙ(ℤ×Port))"/>
<org.eventb.core.scParameter name="l" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.parameter#_RYtJ0OT7EeemadOWCHlIvw" org.eventb.core.type="Link"/>
<org.eventb.core.scParameter name="new_l" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.parameter#_nHIsIARrEei9ocE08JsPSw" org.eventb.core.type="ℙ(ℤ×ℤ×Link)"/>
<org.eventb.core.scParameter name="sci" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.parameter#_S_eIIL4_EeeN0675uvquSw" org.eventb.core.type="ℙ(ℤ×Component)"/>
<org.eventb.core.scParameter name="spi" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.parameter#_S_dhEr4_EeeN0675uvquSw" org.eventb.core.type="ℙ(Component×ℙ(ℤ×Port))"/>
<org.eventb.core.scAction name="new_m" org.eventb.core.assignment="links ≔ links∪({c} × ran(new_l))" org.eventb.core.label="links" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.action#_ov6eYALXEei9ocE08JsPSw"/>
<org.eventb.core.scAction name="new_n" org.eventb.core.assignment="src ≔ src∪{ip⦂ℤ,ic⦂ℤ·ip ↦ ic∈dom(new_l) ∣ new_l(ip ↦ ic) ↦ spi(sci(ic))(ip)}" org.eventb.core.label="nsrc" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.action#_ztHbMAaaEeiFlqW-8GKglg"/>
<org.eventb.core.scAction name="new_o" org.eventb.core.assignment="dst ≔ dst∪{ip⦂ℤ,ic⦂ℤ·ip ↦ ic∈dom(new_l) ∣ new_l(ip ↦ ic) ↦ dpi(dci(ip))(ic)}" org.eventb.core.label="ndst" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.action#_1ZIboAabEeiFlqW-8GKglg"/>
<org.eventb.core.scAction name="new_p" org.eventb.core.assignment="inst2pat_l ≔ inst2pat_l∪(ran(new_l) × {l})" org.eventb.core.label="inst2pat_l" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.action#_1ZIboQabEeiFlqW-8GKglg"/>
<org.eventb.core.scAction name="new_q" org.eventb.core.assignment="c_links_done ≔ c_links_done∪{l ↦ c}" org.eventb.core.label="c_links_done" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_H7W2gPg_EeeeS5KQUtrGlw|org.eventb.core.action#_czs-oAi3EeiFlqW-8GKglg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="to_unfold_p_iu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="apply_pattern" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/mPort.bcm|org.eventb.core.scMachineFile#mPort|org.eventb.core.scEvent#to_unfold_p_it" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw|org.eventb.core.refinesEvent#_K9vXABKbEeqU6uo9ksjEPA"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="ic" org.eventb.core.predicate="inst_components∈components[{Inst}] ⤔ components[{Mdl}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_AkqiQAhGEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="nc" org.eventb.core.predicate="new_components∈components[{Inst}] ∖ dom(inst_components) ↣ Component ∖ ran(components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_AkqiQQhGEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="acycl_inst_components" org.eventb.core.predicate="dom(inst_components) ◁ container;inst_components⊆inst_components;container" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_AkqiQghGEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="acycl_container" org.eventb.core.predicate="container[dom(inst_components)]⊆dom(inst_components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_AkqiQwhGEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="inst_containers_dom" org.eventb.core.predicate="containers[dom(inst_components)]⊆dom(inst_components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_PCNOECCpEeq7BuY4D8yZpw" org.eventb.core.theorem="true"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="inst_containers" org.eventb.core.predicate="dom(inst_components) ◁ containers;inst_components⊆inst_components;containers" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_PCN1ICCpEeq7BuY4D8yZpw" org.eventb.core.theorem="true"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="new_cont" org.eventb.core.predicate="ran(new_components)∩ran(container)=(∅ ⦂ ℙ(Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_vq9m8CC_Eeq7BuY4D8yZpw" org.eventb.core.theorem="true"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="new_conts" org.eventb.core.predicate="ran(new_components)∩ran(containers)=(∅ ⦂ ℙ(Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_vq9m8SC_Eeq7BuY4D8yZpw" org.eventb.core.theorem="true"/>
<org.eventb.core.scGuard name="inst_componentw" org.eventb.core.label="inst_prop" org.eventb.core.predicate="inst_props∈Property ⇸ Property" org.eventb.core.source="/MODELS_INC_V9_VAR/mProperty.bum|org.eventb.core.machineFile#mProperty|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.guard#_btHw0_qwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenty" org.eventb.core.label="ip" org.eventb.core.predicate="inst_ports∈(components;ports)[{Inst}] ⤔ (components;ports)[{Mdl}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.guard#_btI-9PqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componentz" org.eventb.core.label="mp_i" org.eventb.core.predicate="inst_ports[IPort]⊆IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.guard#_btI-9fqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_component{" org.eventb.core.label="mp_o" org.eventb.core.predicate="inst_ports[OPort]⊆OPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.guard#_btI-9vqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_component|" org.eventb.core.label="ports_inst_rel_comp_inst" org.eventb.core.predicate="ports∼[dom(inst_ports)]⊆dom(inst_components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.guard#_btI-9_qwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_component}" org.eventb.core.label="ports_inst_rel_port_comp" org.eventb.core.predicate="inst_ports∼;ports∼;inst_components⊆ports∼" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.guard#_btI--PqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_component~" org.eventb.core.label="np" org.eventb.core.predicate="new_ports∈(components;ports)[{Inst}] ∖ dom(inst_ports) ↣ Port ∖ ran(components;ports)" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.guard#_btI--fqwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu'" org.eventb.core.label="np_i" org.eventb.core.predicate="new_ports[IPort]⊆IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.guard#_knJVMAK2EeiAPf1wPUl3Gw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu(" org.eventb.core.label="np_o" org.eventb.core.predicate="new_ports[OPort]⊆OPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.guard#_OuP8ACxHEeiUbZrF94gIyA" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="inst_componentt" org.eventb.core.assignment="components ≔ components∪({Mdl} × ran(new_components))" org.eventb.core.label="m" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.action#_nECSUA3EEeqU6uo9ksjEPA"/>
<org.eventb.core.scAction name="inst_componentu" org.eventb.core.assignment="container ≔ container∪(new_components∼;container;(inst_components∪new_components))" org.eventb.core.label="f" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.action#_nECSUQ3EEeqU6uo9ksjEPA"/>
<org.eventb.core.scAction name="inst_componentv" org.eventb.core.assignment="containers ≔ containers∪(new_components∼;containers;(new_components∪inst_components);(containers∪(id ⦂ ℙ(Component×Component))))" org.eventb.core.label="c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.action#_suvPACASEeq7BuY4D8yZpw"/>
<org.eventb.core.scAction name="inst_componentx" org.eventb.core.assignment="cProperties ≔ cProperties∪((inst_components∪new_components)∼;cProperties;((id ⦂ ℙ(Property×Property))inst_props))" org.eventb.core.label="prop" org.eventb.core.source="/MODELS_INC_V9_VAR/mProperty.bum|org.eventb.core.machineFile#mProperty|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.action#_bAhyggKxEeiAPf1wPUl3Gw"/>
<org.eventb.core.scAction name="inst_componenu)" org.eventb.core.assignment="ports ≔ ports∪((inst_components∪new_components)∼;ports;(inst_ports∪new_ports))" org.eventb.core.label="p" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.action#_nVtZw_I8EemlHb-ZV1EcBQ"/>
<org.eventb.core.scParameter name="inst_components" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.parameter#_rQ0PgPtxEeectLZKwQfI0A" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.scParameter name="new_components" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.parameter#_h4VmkAKrEeiAPf1wPUl3Gw" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.scParameter name="inst_props" org.eventb.core.source="/MODELS_INC_V9_VAR/mProperty.bum|org.eventb.core.machineFile#mProperty|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.parameter#_btHw0fqwEeectLZKwQfI0A" org.eventb.core.type="ℙ(Property×Property)"/>
<org.eventb.core.scParameter name="inst_ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.parameter#_btKNE_qwEeectLZKwQfI0A" org.eventb.core.type="ℙ(Port×Port)"/>
<org.eventb.core.scParameter name="new_ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_btKNGPqwEeectLZKwQfI0A|org.eventb.core.parameter#_LNbVcAWLEei9ocE08JsPSw" org.eventb.core.type="ℙ(Port×Port)"/>
<org.eventb.core.scGuard name="inst_componenu*" org.eventb.core.label="inst_links_ty" org.eventb.core.predicate="inst_links∈(components;links)[{Inst}] ⤔ (components;links)[{Mdl}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw|org.eventb.core.guard#_Bszp0AsoEeigQsLVMUeRQw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu+" org.eventb.core.label="inst_src" org.eventb.core.predicate="inst_links;src⊆src;inst_ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw|org.eventb.core.guard#_G8ASkAsoEeigQsLVMUeRQw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu," org.eventb.core.label="inst_dst" org.eventb.core.predicate="inst_links;dst⊆dst;inst_ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw|org.eventb.core.guard#_78O84AsoEeigQsLVMUeRQw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu-" org.eventb.core.label="nl" org.eventb.core.predicate="new_links∈(components;links)[{Inst}] ∖ dom(inst_links) ↣ Link ∖ ran(links)" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw|org.eventb.core.guard#_78O84QsoEeigQsLVMUeRQw" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="inst_links" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw|org.eventb.core.parameter#_nHJTMQRrEei9ocE08JsPSw" org.eventb.core.type="ℙ(Link×Link)"/>
<org.eventb.core.scParameter name="new_links" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw|org.eventb.core.parameter#_nxuuQAi-EeiFlqW-8GKglg" org.eventb.core.type="ℙ(Link×Link)"/>
<org.eventb.core.scAction name="inst_componenu." org.eventb.core.assignment="src ≔ src(new_links∼;src;(inst_ports∪new_ports))" org.eventb.core.label="s" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw|org.eventb.core.action#_czuz0gi3EeiFlqW-8GKglg"/>
<org.eventb.core.scAction name="inst_componenu/" org.eventb.core.assignment="dst ≔ dst(new_links∼;dst;(inst_ports∪new_ports))" org.eventb.core.label="d" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw|org.eventb.core.action#_vsWoMAs_EeiJbMmmYBswhA"/>
<org.eventb.core.scAction name="inst_componenu0" org.eventb.core.assignment="links ≔ links∪((inst_components∪new_components)∼;links;new_links)" org.eventb.core.label="l" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_ypJCIflnEeeeS5KQUtrGlw|org.eventb.core.action#_Ce3aEAtCEeiJbMmmYBswhA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="to_unfold_p_iv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="apply_link_pattern" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MODELS_INC_V9_VAR/mPort.bcm|org.eventb.core.scMachineFile#mPort|org.eventb.core.scEvent#to_unfold_p_iu" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw|org.eventb.core.refinesEvent#_K9v-EBKbEeqU6uo9ksjEPA"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="ic" org.eventb.core.predicate="inst_components∈components[{Inst}] ⤔ components[{Mdl}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_AkqiQAhGEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="nc" org.eventb.core.predicate="new_components∈components[{Inst}] ∖ dom(inst_components) ↣ Component ∖ ran(components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_AkqiQQhGEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="acycl_inst_components" org.eventb.core.predicate="dom(inst_components) ◁ container;inst_components⊆inst_components;container" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_AkqiQghGEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="acycl_container" org.eventb.core.predicate="container[dom(inst_components)]⊆dom(inst_components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_AkqiQwhGEeqU6uo9ksjEPA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="inst_containers_dom" org.eventb.core.predicate="containers[dom(inst_components)]⊆dom(inst_components)" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_PCNOECCpEeq7BuY4D8yZpw" org.eventb.core.theorem="true"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="inst_containers" org.eventb.core.predicate="dom(inst_components) ◁ containers;inst_components⊆inst_components;containers" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_PCN1ICCpEeq7BuY4D8yZpw" org.eventb.core.theorem="true"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="new_cont" org.eventb.core.predicate="ran(new_components)∩ran(container)=(∅ ⦂ ℙ(Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_vq9m8CC_Eeq7BuY4D8yZpw" org.eventb.core.theorem="true"/>
<org.eventb.core.scGuard name="." org.eventb.core.label="new_conts" org.eventb.core.predicate="ran(new_components)∩ran(containers)=(∅ ⦂ ℙ(Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.guard#_vq9m8SC_Eeq7BuY4D8yZpw" org.eventb.core.theorem="true"/>
<org.eventb.core.scGuard name="inst_componentw" org.eventb.core.label="inst_prop" org.eventb.core.predicate="inst_props∈Property ⇸ Property" org.eventb.core.source="/MODELS_INC_V9_VAR/mProperty.bum|org.eventb.core.machineFile#mProperty|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.guard#_btHw0_qwEeectLZKwQfI0A" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenty" org.eventb.core.label="comp" org.eventb.core.predicate="comp∈components[{Mdl}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.guard#_nVsyuPI8EemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componentz" org.eventb.core.label="comp_map" org.eventb.core.predicate="ran(inst_components)={comp}" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.guard#_nVsyufI8EemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_component{" org.eventb.core.label="src_subc" org.eventb.core.predicate="src_subc × {comp}⊆container" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.guard#_nVsyuvI8EemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_component|" org.eventb.core.label="dst_subc" org.eventb.core.predicate="dst_subc × {comp}⊆container" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.guard#_nVsyu_I8EemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_component}" org.eventb.core.label="ip" org.eventb.core.predicate="src_ports∈(inst_components∼;ports ▷ IPort)[{comp}] ⤔ ports[src_subc]∩OPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.guard#_nVsyvPI8EemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_component~" org.eventb.core.label="op" org.eventb.core.predicate="dst_ports∈(inst_components∼;ports ▷ OPort)[{comp}] ⤔ ports[dst_subc]∩IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.guard#_nVsyvfI8EemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu'" org.eventb.core.label="np" org.eventb.core.predicate="new_ports∈(components;ports)[{Inst}] ∖ (dom(src_ports)∪dom(src_ports)) ↣ Port ∖ ran(components;ports)" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.guard#_nVsyvvI8EemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu(" org.eventb.core.label="np_i" org.eventb.core.predicate="new_ports[IPort]⊆IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.guard#_nVtZwPI8EemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu)" org.eventb.core.label="np_o" org.eventb.core.predicate="new_ports[OPort]⊆OPort" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.guard#_nVtZwfI8EemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="inst_componentt" org.eventb.core.assignment="components ≔ components∪({Mdl} × ran(new_components))" org.eventb.core.label="m" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.action#_nECSUA3EEeqU6uo9ksjEPA"/>
<org.eventb.core.scAction name="inst_componentu" org.eventb.core.assignment="container ≔ container∪(new_components∼;container;(inst_components∪new_components))" org.eventb.core.label="f" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.action#_nECSUQ3EEeqU6uo9ksjEPA"/>
<org.eventb.core.scAction name="inst_componentv" org.eventb.core.assignment="containers ≔ containers∪(new_components∼;containers;(new_components∪inst_components);(containers∪(id ⦂ ℙ(Component×Component))))" org.eventb.core.label="c" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.action#_suvPACASEeq7BuY4D8yZpw"/>
<org.eventb.core.scAction name="inst_componentx" org.eventb.core.assignment="cProperties ≔ cProperties∪((inst_components∪new_components)∼;cProperties;((id ⦂ ℙ(Property×Property))inst_props))" org.eventb.core.label="prop" org.eventb.core.source="/MODELS_INC_V9_VAR/mProperty.bum|org.eventb.core.machineFile#mProperty|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.action#_bAhyggKxEeiAPf1wPUl3Gw"/>
<org.eventb.core.scAction name="inst_componenu*" org.eventb.core.assignment="ports ≔ ports∪((inst_components∪new_components)∼;ports;new_ports)" org.eventb.core.label="p" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.action#_LcSJoBKaEeqU6uo9ksjEPA"/>
<org.eventb.core.scParameter name="inst_components" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.parameter#_rQ0PgPtxEeectLZKwQfI0A" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.scParameter name="new_components" org.eventb.core.source="/MODELS_INC_V9_VAR/mComponent.bum|org.eventb.core.machineFile#mComponent|org.eventb.core.event#_O1W_yfqmEeectLZKwQfI0A|org.eventb.core.parameter#_h4VmkAKrEeiAPf1wPUl3Gw" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.scParameter name="inst_props" org.eventb.core.source="/MODELS_INC_V9_VAR/mProperty.bum|org.eventb.core.machineFile#mProperty|org.eventb.core.event#_btKNEfqwEeectLZKwQfI0A|org.eventb.core.parameter#_btHw0fqwEeectLZKwQfI0A" org.eventb.core.type="ℙ(Property×Property)"/>
<org.eventb.core.scParameter name="comp" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.parameter#_nVsysvI8EemlHb-ZV1EcBQ" org.eventb.core.type="Component"/>
<org.eventb.core.scParameter name="dst_ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.parameter#_nVsytvI8EemlHb-ZV1EcBQ" org.eventb.core.type="ℙ(Port×Port)"/>
<org.eventb.core.scParameter name="dst_subc" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.parameter#_nVsytPI8EemlHb-ZV1EcBQ" org.eventb.core.type="ℙ(Component)"/>
<org.eventb.core.scParameter name="new_ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.parameter#_nVsyt_I8EemlHb-ZV1EcBQ" org.eventb.core.type="ℙ(Port×Port)"/>
<org.eventb.core.scParameter name="src_ports" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.parameter#_nVsytfI8EemlHb-ZV1EcBQ" org.eventb.core.type="ℙ(Port×Port)"/>
<org.eventb.core.scParameter name="src_subc" org.eventb.core.source="/MODELS_INC_V9_VAR/mPort.bum|org.eventb.core.machineFile#mPort|org.eventb.core.event#_YUG9oAKzEeiAPf1wPUl3Gw|org.eventb.core.parameter#_nVsys_I8EemlHb-ZV1EcBQ" org.eventb.core.type="ℙ(Component)"/>
<org.eventb.core.scGuard name="inst_componenu+" org.eventb.core.label="inst_links_ty" org.eventb.core.predicate="inst_links⊆links[{comp}]" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw|org.eventb.core.guard#_F143NPJAEemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu," org.eventb.core.label="inst_src" org.eventb.core.predicate="src[inst_links]=dom(src_ports)" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw|org.eventb.core.guard#_F143NfJAEemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu-" org.eventb.core.label="inst_dst" org.eventb.core.predicate="dst[inst_links]=dom(dst_ports)" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw|org.eventb.core.guard#_F143NvJAEemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="inst_componenu." org.eventb.core.label="nl" org.eventb.core.predicate="new_links∈(components;links)[{Inst}] ↣ Link ∖ ran(links)" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw|org.eventb.core.guard#_F143N_JAEemlHb-ZV1EcBQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="inst_links" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw|org.eventb.core.parameter#_F143MvJAEemlHb-ZV1EcBQ" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.scParameter name="new_links" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw|org.eventb.core.parameter#_F143M_JAEemlHb-ZV1EcBQ" org.eventb.core.type="ℙ(Link×Link)"/>
<org.eventb.core.scAction name="inst_componenu/" org.eventb.core.assignment="src ≔ (inst_links ⩤ src)(new_links∼;src;new_ports)" org.eventb.core.label="s" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw|org.eventb.core.action#_F143OPJAEemlHb-ZV1EcBQ"/>
<org.eventb.core.scAction name="inst_componenu0" org.eventb.core.assignment="dst ≔ (inst_links ⩤ dst)(new_links∼;dst;new_ports)" org.eventb.core.label="d" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw|org.eventb.core.action#_F143OfJAEemlHb-ZV1EcBQ"/>
<org.eventb.core.scAction name="inst_componenu1" org.eventb.core.assignment="links ≔ (links ⩥ inst_links)∪((inst_components∪new_components)∼;links;new_links)" org.eventb.core.label="l" org.eventb.core.source="/MODELS_INC_V9_VAR/mLink.bum|org.eventb.core.machineFile#mLink|org.eventb.core.event#_u6P4gAK9EeiAPf1wPUl3Gw|org.eventb.core.action#_F143OvJAEemlHb-ZV1EcBQ"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>